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 33909

Description: Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33914. (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 6102	. . 3 $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
3		simp1l 1012	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4		simp22l 1107	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5		hllat 33008	. . . . . 6
6	3, 5	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simp23 1023	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		eqid 2443	. . . . . . 7
9		cdleme11.a	. . . . . . 7
10	8, 9	atbase 32934	. . . . . 6
11	7, 10	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		simp1 988	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simp21 1021	. . . . . 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 33854	. . . . . 6 $/\$ $/\$ $/\$
20	12, 13, 4, 19	syl3anc 1218	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21	8, 15	latjcl 15221	. . . . 5 $/\$ $/\$ $.\/$
22	6, 11, 20, 21	syl3anc 1218	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	8, 9	atbase 32934	. . . . . 6
24	4, 23	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	8, 9	atbase 32934	. . . . . . . 8
26	13, 25	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27	8, 15	latjcl 15221	. . . . . . 7 $/\$ $/\$ $.\/$
28	6, 26, 11, 27	syl3anc 1218	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29		simp1r 1013	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	8, 17	lhpbase 33642	. . . . . . 7
31	29, 30	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	8, 16	latmcl 15222	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
33	6, 28, 31, 32	syl3anc 1218	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
34	8, 15	latjcl 15221	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
35	6, 24, 33, 34	syl3anc 1218	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
36	8, 14, 15	latlej1 15230	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
37	6, 24, 33, 36	syl3anc 1218	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
38	8, 14, 15, 16, 9	atmod1i1 33501	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
39	3, 4, 22, 35, 37, 38	syl131anc 1231	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
40	2, 39	syl5eq 2487	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
41		simp22 1022	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	14, 15, 16, 9, 17, 18	cdleme0cq 33859	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
43	12, 13, 41, 42	syl12anc 1216	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
44	43	oveq2d 6107	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
45	8, 15	latj12 15266	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
46	6, 24, 11, 20, 45	syl13anc 1220	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
47	8, 15	latj13 15268	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
48	6, 24, 26, 11, 47	syl13anc 1220	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
49	44, 46, 48	3eqtr4d 2485	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
50	49	oveq1d 6106	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
51	8, 14, 16	latmle1 15246	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
52	6, 28, 31, 51	syl3anc 1218	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
53	8, 14, 15	latjlej2 15236	. . . . . 6 $/\$ $.\/$ $./\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
54	6, 33, 28, 24, 53	syl13anc 1220	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
55	52, 54	mpd 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
56	8, 15	latjcl 15221	. . . . . 6 $/\$ $/\$ $.\/$ $.\/$ $.\/$
57	6, 24, 28, 56	syl3anc 1218	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
58	8, 14, 16	latleeqm2 15250	. . . . 5 $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
59	6, 35, 57, 58	syl3anc 1218	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
60	55, 59	mpbid 210	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
61		cdleme11.c	. . . 4 $.\/$ $./\$
62	61	oveq2i 6102	. . 3 $.\/$ $.\/$ $.\/$ $./\$
63	60, 62	syl6eqr 2493	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
64	40, 50, 63	3eqtrd 2479	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

wne 2606 class class class wbr 4292

cfv 5418 (class class class)co 6091

cbs 14174

cple 14245

cjn 15114

cmee 15115

clat 15215

catm 32908

chlt 32995

clh 33628

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-reu 2722 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-op 3884 df-uni 4092 df-iun 4173 df-iin 4174 df-br 4293 df-opab 4351 df-mpt 4352 df-id 4636 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-1st 6577 df-2nd 6578 df-poset 15116 df-plt 15128 df-lub 15144 df-glb 15145 df-join 15146 df-meet 15147 df-p0 15209 df-p1 15210 df-lat 15216 df-clat 15278 df-oposet 32821 df-ol 32823 df-oml 32824 df-covers 32911 df-ats 32912 df-atl 32943 df-cvlat 32967 df-hlat 32996 df-psubsp 33147 df-pmap 33148 df-padd 33440 df-lhyp 33632

This theorem is referenced by: cdleme11h 33910 cdleme11j 33911 cdleme15a 33918

W3C validator