cdleme11g - Mathbox for Norm Megill

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

Theorem cdleme11g 33264

Description: Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33269. (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 6245	. . 3 $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
3		simp1l 1021	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4		simp22l 1116	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5		hllat 32362	. . . . . 6
6	3, 5	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simp23 1032	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		eqid 2402	. . . . . . 7
9		cdleme11.a	. . . . . . 7
10	8, 9	atbase 32288	. . . . . 6
11	7, 10	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		simp1 997	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simp21 1030	. . . . . 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 33209	. . . . . 6 $/\$ $/\$ $/\$
20	12, 13, 4, 19	syl3anc 1230	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21	8, 15	latjcl 15897	. . . . 5 $/\$ $/\$ $.\/$
22	6, 11, 20, 21	syl3anc 1230	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	8, 9	atbase 32288	. . . . . 6
24	4, 23	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	8, 9	atbase 32288	. . . . . . . 8
26	13, 25	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	8, 15	latjcl 15897	. . . . . . 7 $/\$ $/\$ $.\/$
28	6, 26, 11, 27	syl3anc 1230	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29		simp1r 1022	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	8, 17	lhpbase 32996	. . . . . . 7
31	29, 30	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	8, 16	latmcl 15898	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
33	6, 28, 31, 32	syl3anc 1230	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
34	8, 15	latjcl 15897	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
35	6, 24, 33, 34	syl3anc 1230	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
36	8, 14, 15	latlej1 15906	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
37	6, 24, 33, 36	syl3anc 1230	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
38	8, 14, 15, 16, 9	atmod1i1 32855	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
39	3, 4, 22, 35, 37, 38	syl131anc 1243	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
40	2, 39	syl5eq 2455	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
41		simp22 1031	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	14, 15, 16, 9, 17, 18	cdleme0cq 33214	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
43	12, 13, 41, 42	syl12anc 1228	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
44	43	oveq2d 6250	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
45	8, 15	latj12 15942	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
46	6, 24, 11, 20, 45	syl13anc 1232	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
47	8, 15	latj13 15944	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
48	6, 24, 26, 11, 47	syl13anc 1232	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
49	44, 46, 48	3eqtr4d 2453	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
50	49	oveq1d 6249	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
51	8, 14, 16	latmle1 15922	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
52	6, 28, 31, 51	syl3anc 1230	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
53	8, 14, 15	latjlej2 15912	. . . . . 6 $/\$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
54	6, 33, 28, 24, 53	syl13anc 1232	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
55	52, 54	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
56	8, 15	latjcl 15897	. . . . . 6 $/\$ $/\$ $.\/$ $.\/$ $.\/$
57	6, 24, 28, 56	syl3anc 1230	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
58	8, 14, 16	latleeqm2 15926	. . . . 5 $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
59	6, 35, 57, 58	syl3anc 1230	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
60	55, 59	mpbid 210	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
61		cdleme11.c	. . . 4 $.\/$ $./\$
62	61	oveq2i 6245	. . 3 $.\/$ $.\/$ $.\/$ $./\$
63	60, 62	syl6eqr 2461	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
64	40, 50, 63	3eqtrd 2447	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wne 2598 class class class wbr 4394

cfv 5525 (class class class)co 6234

cbs 14733

cple 14808

cjn 15789

cmee 15790

clat 15891

catm 32262

chlt 32349

clh 32982

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6530

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-ral 2758 df-rex 2759 df-reu 2760 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-op 3978 df-uni 4191 df-iun 4272 df-iin 4273 df-br 4395 df-opab 4453 df-mpt 4454 df-id 4737 df-xp 4948 df-rel 4949 df-cnv 4950 df-co 4951 df-dm 4952 df-rn 4953 df-res 4954 df-ima 4955 df-iota 5489 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-riota 6196 df-ov 6237 df-oprab 6238 df-mpt2 6239 df-1st 6738 df-2nd 6739 df-preset 15773 df-poset 15791 df-plt 15804 df-lub 15820 df-glb 15821 df-join 15822 df-meet 15823 df-p0 15885 df-p1 15886 df-lat 15892 df-clat 15954 df-oposet 32175 df-ol 32177 df-oml 32178 df-covers 32265 df-ats 32266 df-atl 32297 df-cvlat 32321 df-hlat 32350 df-psubsp 32501 df-pmap 32502 df-padd 32794 df-lhyp 32986

This theorem is referenced by: cdleme11h 33265 cdleme11j 33266 cdleme15a 33273

W3C validator