cdleme11g - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdleme11g		Structured version Visualization version Unicode version

Theorem cdleme11g 33843

Description: Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33848. (Contributed by NM, 14-Jun-2012.)

**Hypotheses**
Ref	Expression
cdleme11.l
cdleme11.j	$.\/$
cdleme11.m	$./\$
cdleme11.a
cdleme11.h
cdleme11.u	$.\/$ $./\$
cdleme11.c	$.\/$ $./\$
cdleme11.d	$.\/$ $./\$
cdleme11.f	$.\/$ $./\$ $.\/$ $.\/$ $./\$

**Assertion**
Ref	Expression
cdleme11g	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

**Proof of Theorem cdleme11g**
Step	Hyp	Ref	Expression
1		cdleme11.f	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
2	1	oveq2i 6306	. . 3 $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
3		simp1l 1033	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4		simp22l 1128	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5		hllat 32941	. . . . . 6
6	3, 5	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simp23 1044	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		eqid 2453	. . . . . . 7
9		cdleme11.a	. . . . . . 7
10	8, 9	atbase 32867	. . . . . 6
11	7, 10	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		simp1 1009	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simp21 1042	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		cdleme11.l	. . . . . . 7
15		cdleme11.j	. . . . . . 7 $.\/$
16		cdleme11.m	. . . . . . 7 $./\$
17		cdleme11.h	. . . . . . 7
18		cdleme11.u	. . . . . . 7 $.\/$ $./\$
19	14, 15, 16, 9, 17, 18, 8	cdleme0aa 33788	. . . . . 6 $/\$ $/\$ $/\$
20	12, 13, 4, 19	syl3anc 1269	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21	8, 15	latjcl 16309	. . . . 5 $/\$ $/\$ $.\/$
22	6, 11, 20, 21	syl3anc 1269	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	8, 9	atbase 32867	. . . . . 6
24	4, 23	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	8, 9	atbase 32867	. . . . . . . 8
26	13, 25	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	8, 15	latjcl 16309	. . . . . . 7 $/\$ $/\$ $.\/$
28	6, 26, 11, 27	syl3anc 1269	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29		simp1r 1034	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	8, 17	lhpbase 33575	. . . . . . 7
31	29, 30	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	8, 16	latmcl 16310	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
33	6, 28, 31, 32	syl3anc 1269	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
34	8, 15	latjcl 16309	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
35	6, 24, 33, 34	syl3anc 1269	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
36	8, 14, 15	latlej1 16318	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
37	6, 24, 33, 36	syl3anc 1269	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
38	8, 14, 15, 16, 9	atmod1i1 33434	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
39	3, 4, 22, 35, 37, 38	syl131anc 1282	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
40	2, 39	syl5eq 2499	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
41		simp22 1043	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	14, 15, 16, 9, 17, 18	cdleme0cq 33793	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
43	12, 13, 41, 42	syl12anc 1267	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
44	43	oveq2d 6311	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
45	8, 15	latj12 16354	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
46	6, 24, 11, 20, 45	syl13anc 1271	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
47	8, 15	latj13 16356	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
48	6, 24, 26, 11, 47	syl13anc 1271	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
49	44, 46, 48	3eqtr4d 2497	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
50	49	oveq1d 6310	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
51	8, 14, 16	latmle1 16334	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
52	6, 28, 31, 51	syl3anc 1269	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
53	8, 14, 15	latjlej2 16324	. . . . . 6 $/\$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
54	6, 33, 28, 24, 53	syl13anc 1271	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
55	52, 54	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
56	8, 15	latjcl 16309	. . . . . 6 $/\$ $/\$ $.\/$ $.\/$ $.\/$
57	6, 24, 28, 56	syl3anc 1269	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
58	8, 14, 16	latleeqm2 16338	. . . . 5 $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
59	6, 35, 57, 58	syl3anc 1269	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
60	55, 59	mpbid 214	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
61		cdleme11.c	. . . 4 $.\/$ $./\$
62	61	oveq2i 6306	. . 3 $.\/$ $.\/$ $.\/$ $./\$
63	60, 62	syl6eqr 2505	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
64	40, 50, 63	3eqtrd 2491	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 986

wceq 1446

wcel 1889

wne 2624 class class class wbr 4405

cfv 5585 (class class class)co 6295

cbs 15133

cple 15209

cjn 16201

cmee 16202

clat 16303

catm 32841

chlt 32928

clh 33561

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-rep 4518 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-reu 2746 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-op 3977 df-uni 4202 df-iun 4283 df-iin 4284 df-br 4406 df-opab 4465 df-mpt 4466 df-id 4752 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-1st 6798 df-2nd 6799 df-preset 16185 df-poset 16203 df-plt 16216 df-lub 16232 df-glb 16233 df-join 16234 df-meet 16235 df-p0 16297 df-p1 16298 df-lat 16304 df-clat 16366 df-oposet 32754 df-ol 32756 df-oml 32757 df-covers 32844 df-ats 32845 df-atl 32876 df-cvlat 32900 df-hlat 32929 df-psubsp 33080 df-pmap 33081 df-padd 33373 df-lhyp 33565

This theorem is referenced by: cdleme11h 33844 cdleme11j 33845 cdleme15a 33852

W3C validator