cdlemg33a - Mathbox for Norm Megill

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

Theorem cdlemg33a 36307

Description: TODO: Fix comment. (Contributed by NM, 29-May-2013.)

**Hypotheses**
Ref	Expression
cdlemg12.l
cdlemg12.j	$.\/$
cdlemg12.m	$./\$
cdlemg12.a
cdlemg12.h
cdlemg12.t
cdlemg12b.r
cdlemg31.n	$.\/$ $./\$ $.\/$
cdlemg33.o	$.\/$ $./\$ $.\/$

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

Distinct variable groups:

$.\/$ ,

, $.\/$

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

) $.\/$ (

)

(

)

(

) $./\$ (

)

(

)

(

)

(

)

**Proof of Theorem cdlemg33a**
Step	Hyp	Ref	Expression
1		simp11 1027	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
2		simp12 1028	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
3		simp13 1029	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
4		simp22l 1116	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
5		simp21 1030	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
6		simp23l 1118	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
7		simp32 1034	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
8		cdlemg12.l	. . . . . 6
9		cdlemg12.j	. . . . . 6 $.\/$
10		cdlemg12.m	. . . . . 6 $./\$
11		cdlemg12.a	. . . . . 6
12		cdlemg12.h	. . . . . 6
13		cdlemg12.t	. . . . . 6
14		cdlemg12b.r	. . . . . 6
15		cdlemg31.n	. . . . . 6 $.\/$ $./\$ $.\/$
16	8, 9, 10, 11, 12, 13, 14, 15	cdlemg31d 36301	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17	1, 2, 3, 5, 6, 7, 4, 16	syl133anc 1252	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
18	4, 17	jca 532	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
19		simp31l 1120	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
20		simp22r 1117	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
21		simp31r 1121	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
22	20, 21	jca 532	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
23		simp33 1035	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
24	8, 9, 11, 12	4atex3 35680	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$
25	1, 2, 3, 18, 19, 22, 23, 24	syl133anc 1252	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		idd 24	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
27		idd 24	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
28		simp12l 1110	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
29		simp13l 1112	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
30		simp21l 1114	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
31	8, 9, 10, 11, 12, 13, 14, 15	cdlemg31a 36298	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
32	1, 28, 29, 30, 6, 31	syl122anc 1238	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
33		simp23r 1119	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
34		cdlemg33.o	. . . . . . . . . . 11 $.\/$ $./\$ $.\/$
35	8, 9, 10, 11, 12, 13, 14, 34	cdlemg31a 36298	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
36	1, 28, 29, 30, 33, 35	syl122anc 1238	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
37		simp11l 1108	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
38		hllat 34963	. . . . . . . . . . 11
39	37, 38	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
40		eqid 2443	. . . . . . . . . . . 12
41	40, 11	atbase 34889	. . . . . . . . . . 11
42	4, 41	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
43	40, 9, 11	hlatjcl 34966	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
44	37, 28, 30, 43	syl3anc 1229	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
45	40, 11	atbase 34889	. . . . . . . . . . 11
46	20, 45	syl 16	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
47	40, 8, 9	latjlej12 15676	. . . . . . . . . 10 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
48	39, 42, 44, 46, 44, 47	syl122anc 1238	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
49	32, 36, 48	mp2and 679	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
50	40, 9	latjidm 15683	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
51	39, 44, 50	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
52	49, 51	breqtrd 4461	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
53	52	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
54	39	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
55	40, 11	atbase 34889	. . . . . . . 8
56	55	adantl 466	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$
57	40, 9, 11	hlatjcl 34966	. . . . . . . . 9 $/\$ $/\$ $.\/$
58	37, 4, 20, 57	syl3anc 1229	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
59	58	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
60	44	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
61	40, 8	lattr 15665	. . . . . . 7 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
62	54, 56, 59, 60, 61	syl13anc 1231	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
63	53, 62	mpan2d 674	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
64	26, 27, 63	3anim123d 1307	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
65	64	anim2d 565	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
66	65	reximdva 2918	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
67	25, 66	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 974

wceq 1383

wcel 1804

wne 2638

wrex 2794 class class class wbr 4437

cfv 5578 (class class class)co 6281

cbs 14614

cple 14686

cjn 15552

cmee 15553

clat 15654

catm 34863

chlt 34950

clh 35583

cltrn 35700

ctrl 35758

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-ral 2798 df-rex 2799 df-reu 2800 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-op 4021 df-uni 4235 df-iun 4317 df-iin 4318 df-br 4438 df-opab 4496 df-mpt 4497 df-id 4785 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-1st 6785 df-2nd 6786 df-map 7424 df-preset 15536 df-poset 15554 df-plt 15567 df-lub 15583 df-glb 15584 df-join 15585 df-meet 15586 df-p0 15648 df-p1 15649 df-lat 15655 df-clat 15717 df-oposet 34776 df-ol 34778 df-oml 34779 df-covers 34866 df-ats 34867 df-atl 34898 df-cvlat 34922 df-hlat 34951 df-llines 35097 df-lplanes 35098 df-psubsp 35102 df-pmap 35103 df-padd 35395 df-lhyp 35587 df-laut 35588 df-ldil 35703 df-ltrn 35704 df-trl 35759

This theorem is referenced by: cdlemg33b 36308

W3C validator