cdlemg12g - Mathbox for Norm Megill

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

Theorem cdlemg12g 34133

Description: TODO: FIX COMMENT TODO: Combine with cdlemg12f 34132. (Contributed by NM, 6-May-2013.)

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

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

**Proof of Theorem cdlemg12g**
Step	Hyp	Ref	Expression
1		simp11l 1099	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
2		hlop 32847	. . 3
3	1, 2	syl 16	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
4		hllat 32848	. . . 4
5	1, 4	syl 16	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
6		simp12l 1101	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
7		simp11 1018	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$
8		simp21 1021	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
9		simp22 1022	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
10		cdlemg12.l	. . . . . 6
11		cdlemg12.a	. . . . . 6
12		cdlemg12.h	. . . . . 6
13		cdlemg12.t	. . . . . 6
14	10, 11, 12, 13	ltrncoat 33628	. . . . 5 $/\$ $/\$ $/\$ $/\$
15	7, 8, 9, 6, 14	syl121anc 1223	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
16		eqid 2438	. . . . 5
17		cdlemg12.j	. . . . 5 $.\/$
18	16, 17, 11	hlatjcl 32851	. . . 4 $/\$ $/\$ $.\/$
19	1, 6, 15, 18	syl3anc 1218	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
20		simp13l 1103	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
21	10, 11, 12, 13	ltrncoat 33628	. . . . 5 $/\$ $/\$ $/\$ $/\$
22	7, 8, 9, 20, 21	syl121anc 1223	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
23	16, 17, 11	hlatjcl 32851	. . . 4 $/\$ $/\$ $.\/$
24	1, 20, 22, 23	syl3anc 1218	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
25		cdlemg12.m	. . . 4 $./\$
26	16, 25	latmcl 15214	. . 3 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
27	5, 19, 24, 26	syl3anc 1218	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
28		simp12 1019	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$
29		simp13 1020	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$
30		simp33 1026	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
31	10, 17, 25, 11, 12, 13	cdlemg11a 34121	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
32	31	necomd 2690	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
33	7, 28, 29, 8, 9, 30, 32	syl123anc 1235	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
34	10, 17, 25, 11, 12	lhpat 33527	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
35	7, 28, 15, 33, 34	syl112anc 1222	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$
36	17, 11	hlatjcom 32852	. . . . 5 $/\$ $/\$ $.\/$ $.\/$
37	1, 6, 15, 36	syl3anc 1218	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
38	17, 11	hlatjcom 32852	. . . . 5 $/\$ $/\$ $.\/$ $.\/$
39	1, 20, 22, 38	syl3anc 1218	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
40	37, 39	oveq12d 6104	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
41		simp1 988	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simp2 989	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$
43		simp31l 1111	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
44		simp31r 1112	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
45		simp32 1025	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
46		cdlemg12b.r	. . . . 5
47		eqid 2438	. . . . 5
48	10, 17, 25, 11, 12, 13, 46, 47	cdlemg12e 34131	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
49	41, 42, 43, 44, 45, 48	syl113anc 1230	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
50	40, 49	eqnetrd 2621	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
51	10, 17, 25, 11, 12, 13, 46	cdlemg12f 34132	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
52	16, 10, 47, 11	leat2 32779	. 2 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
53	3, 27, 35, 50, 51, 52	syl32anc 1226	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1369

wcel 1756

wne 2601 class class class wbr 4287

cfv 5413 (class class class)co 6086

cbs 14166

cple 14237

cjn 15106

cmee 15107

cp0 15199

clat 15207

cops 32657

catm 32748

chlt 32835

clh 33468

cltrn 33585

ctrl 33642

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 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-riotaBAD 32444

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-op 3879 df-uni 4087 df-iun 4168 df-iin 4169 df-br 4288 df-opab 4346 df-mpt 4347 df-id 4631 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-1st 6572 df-2nd 6573 df-undef 6784 df-map 7208 df-poset 15108 df-plt 15120 df-lub 15136 df-glb 15137 df-join 15138 df-meet 15139 df-p0 15201 df-p1 15202 df-lat 15208 df-clat 15270 df-oposet 32661 df-ol 32663 df-oml 32664 df-covers 32751 df-ats 32752 df-atl 32783 df-cvlat 32807 df-hlat 32836 df-llines 32982 df-lplanes 32983 df-lvols 32984 df-lines 32985 df-psubsp 32987 df-pmap 32988 df-padd 33280 df-lhyp 33472 df-laut 33473 df-ldil 33588 df-ltrn 33589 df-trl 33643

This theorem is referenced by: cdlemg12 34134

W3C validator