cdlemc6 - Mathbox for Norm Megill

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

Theorem cdlemc6 30690

Description: Lemma for cdlemc 30691. (Contributed by NM, 26-May-2012.)

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

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

**Proof of Theorem cdlemc6**
Step	Hyp	Ref	Expression
1		simp1l 981	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
2		simp22l 1076	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
3		simp23l 1078	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4		cdlemc3.j	. . . . . 6 $.\/$
5		cdlemc3.a	. . . . . 6
6	4, 5	hlatjcom 29862	. . . . 5 $/\$ $/\$ $.\/$ $.\/$
7	1, 2, 3, 6	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
8	7	oveq2d 6064	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $.\/$ $./\$ $.\/$
9		hllat 29858	. . . . 5
10	1, 9	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		eqid 2412	. . . . . 6
12	11, 5	atbase 29784	. . . . 5
13	3, 12	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14	11, 5	atbase 29784	. . . . 5
15	2, 14	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		cdlemc3.m	. . . . 5 $./\$
17	11, 4, 16	latabs2 14480	. . . 4 $/\$ $/\$ $./\$ $.\/$
18	10, 13, 15, 17	syl3anc 1184	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $.\/$
19	8, 18	eqtrd 2444	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $./\$ $.\/$
20		simp1 957	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		simp22 991	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		simp21 990	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
23		simp3 959	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24		cdlemc3.l	. . . . . . 7
25		eqid 2412	. . . . . . 7
26		cdlemc3.h	. . . . . . 7
27		cdlemc3.t	. . . . . . 7
28		cdlemc3.r	. . . . . . 7
29	24, 25, 5, 26, 27, 28	trl0 30664	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
30	20, 21, 22, 23, 29	syl112anc 1188	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31	30	oveq2d 6064	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
32		hlol 29856	. . . . . 6
33	1, 32	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	11, 4, 25	olj01 29720	. . . . 5 $/\$ $.\/$
35	33, 13, 34	syl2anc 643	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
36	31, 35	eqtrd 2444	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
37	23	oveq1d 6063	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
38	11, 4, 5	hlatjcl 29861	. . . . . . 7 $/\$ $/\$ $.\/$
39	1, 2, 3, 38	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
40		simp1r 982	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	11, 26	lhpbase 30492	. . . . . . 7
42	40, 41	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	11, 16	latmcl 14443	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
44	10, 39, 42, 43	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
45	11, 4	latjcom 14451	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
46	10, 15, 44, 45	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$
47	24, 4, 5	hlatlej1 29869	. . . . . . 7 $/\$ $/\$ $.\/$
48	1, 2, 3, 47	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49	11, 24, 4, 16, 5	atmod2i1 30355	. . . . . 6 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
50	1, 2, 39, 42, 48, 49	syl131anc 1197	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
51		eqid 2412	. . . . . . . 8
52	24, 4, 51, 5, 26	lhpjat1 30514	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$
53	1, 40, 21, 52	syl21anc 1183	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
54	53	oveq2d 6064	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
55	11, 16, 51	olm11 29722	. . . . . 6 $/\$ $.\/$ $.\/$ $./\$ $.\/$
56	33, 39, 55	syl2anc 643	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$
57	50, 54, 56	3eqtrd 2448	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$
58	37, 46, 57	3eqtrd 2448	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
59	36, 58	oveq12d 6066	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$
60	24, 5, 26, 27	ltrnateq 30675	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61	19, 59, 60	3eqtr4rd 2455	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721 class class class wbr 4180

cfv 5421 (class class class)co 6048

cbs 13432

cple 13499

cjn 14364

cmee 14365

cp0 14429

cp1 14430

clat 14437

col 29669

catm 29758

chlt 29845

clh 30478

cltrn 30595

ctrl 30652

This theorem is referenced by: cdlemc 30691

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2393 ax-rep 4288 ax-sep 4298 ax-nul 4306 ax-pow 4345 ax-pr 4371 ax-un 4668

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2266 df-mo 2267 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-ne 2577 df-nel 2578 df-ral 2679 df-rex 2680 df-reu 2681 df-rab 2683 df-v 2926 df-sbc 3130 df-csb 3220 df-dif 3291 df-un 3293 df-in 3295 df-ss 3302 df-nul 3597 df-if 3708 df-pw 3769 df-sn 3788 df-pr 3789 df-op 3791 df-uni 3984 df-iun 4063 df-iin 4064 df-br 4181 df-opab 4235 df-mpt 4236 df-id 4466 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5385 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-ov 6051 df-oprab 6052 df-mpt2 6053 df-1st 6316 df-2nd 6317 df-undef 6510 df-riota 6516 df-map 6987 df-poset 14366 df-plt 14378 df-lub 14394 df-glb 14395 df-join 14396 df-meet 14397 df-p0 14431 df-p1 14432 df-lat 14438 df-clat 14500 df-oposet 29671 df-ol 29673 df-oml 29674 df-covers 29761 df-ats 29762 df-atl 29793 df-cvlat 29817 df-hlat 29846 df-psubsp 29997 df-pmap 29998 df-padd 30290 df-lhyp 30482 df-laut 30483 df-ldil 30598 df-ltrn 30599 df-trl 30653

W3C validator