cdleme32e - Mathbox for Norm Megill

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

Theorem cdleme32e 35116

Description: Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)

**Hypotheses**
Ref	Expression
cdleme32.b
cdleme32.l
cdleme32.j	$.\/$
cdleme32.m	$./\$
cdleme32.a
cdleme32.h
cdleme32.u	$.\/$ $./\$
cdleme32.c	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme32.d	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme32.e	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme32.i	$/\$ $.\/$
cdleme32.n	$.\/$
cdleme32.o	$/\$ $.\/$ $./\$ $.\/$ $./\$
cdleme32.f	$/\$

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

Distinct variable groups:

$.\/$ ,

$./\$ ,

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem cdleme32e**
Step	Hyp	Ref	Expression
1		simp23l 1112	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
2	1	pm2.24d 143	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
3		simp11l 1102	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
4		hllat 34035	. . . . . 6
5	3, 4	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
6		simp21l 1108	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
7		simp11r 1103	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
8		cdleme32.b	. . . . . . 7
9		cdleme32.h	. . . . . . 7
10	8, 9	lhpbase 34669	. . . . . 6
11	7, 10	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
12		cdleme32.l	. . . . . 6
13		cdleme32.m	. . . . . 6 $./\$
14	8, 12, 13	latleeqm1 15555	. . . . 5 $/\$ $/\$ $./\$
15	5, 6, 11, 14	syl3anc 1223	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
16	8, 13	latmcl 15528	. . . . . . 7 $/\$ $/\$ $./\$
17	5, 6, 11, 16	syl3anc 1223	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
18		simp21r 1109	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
19	8, 13	latmcl 15528	. . . . . . 7 $/\$ $/\$ $./\$
20	5, 18, 11, 19	syl3anc 1223	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
21		simp11 1021	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
22		simp12 1022	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
23		simp13 1023	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
24		simp31 1027	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
25		cdleme32.j	. . . . . . . . 9 $.\/$
26		cdleme32.a	. . . . . . . . 9
27		cdleme32.u	. . . . . . . . 9 $.\/$ $./\$
28		cdleme32.c	. . . . . . . . 9 $.\/$ $./\$ $.\/$ $.\/$ $./\$
29		cdleme32.d	. . . . . . . . 9 $.\/$ $./\$ $.\/$ $.\/$ $./\$
30		cdleme32.e	. . . . . . . . 9 $.\/$ $./\$ $.\/$ $.\/$ $./\$
31		cdleme32.i	. . . . . . . . 9 $/\$ $.\/$
32		cdleme32.n	. . . . . . . . 9 $.\/$
33	8, 12, 25, 13, 26, 9, 27, 28, 29, 30, 31, 32	cdleme27cl 35037	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	21, 22, 23, 24, 1, 33	syl122anc 1232	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
35	8, 25	latjcl 15527	. . . . . . 7 $/\$ $/\$ $./\$ $.\/$ $./\$
36	5, 34, 20, 35	syl3anc 1223	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
37		simp33 1029	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
38	8, 12, 13	latmlem1 15557	. . . . . . . 8 $/\$ $/\$ $/\$ $./\$ $./\$
39	5, 6, 18, 11, 38	syl13anc 1225	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $./\$
40	37, 39	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $./\$
41	8, 12, 25	latlej2 15537	. . . . . . 7 $/\$ $/\$ $./\$ $./\$ $.\/$ $./\$
42	5, 34, 20, 41	syl3anc 1223	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
43	8, 12, 5, 17, 20, 36, 40, 42	lattrd 15534	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
44		breq1 4443	. . . . 5 $./\$ $./\$ $.\/$ $./\$ $.\/$ $./\$
45	43, 44	syl5ibcom 220	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
46	15, 45	sylbid 215	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
47		simp22 1025	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
48		pm4.53 492	. . . 4 $/\$ $\/$
49	47, 48	sylib 196	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $\/$
50	2, 46, 49	mpjaod 381	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
51		cdleme32.f	. . . 4 $/\$
52	51	cdleme31fv2 35064	. . 3 $/\$ $/\$
53	6, 47, 52	syl2anc 661	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
54		simp1 991	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		simp23 1026	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
56		simp32 1028	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
57		cdleme32.o	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $./\$
58	8, 12, 25, 13, 26, 9, 27, 28, 29, 30, 31, 32, 57, 51	cdleme32a 35112	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
59	54, 18, 55, 24, 56, 58	syl122anc 1232	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
60	50, 53, 59	3brtr4d 4470	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 968

wceq 1374

wcel 1762

wne 2655

wral 2807

cif 3932 class class class wbr 4440

cmpt 4498

cfv 5579

crio 6235 (class class class)co 6275

cbs 14479

cple 14551

cjn 15420

cmee 15421

clat 15521

catm 33935

chlt 34022

clh 34655

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-riotaBAD 33631

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-op 4027 df-uni 4239 df-iun 4320 df-iin 4321 df-br 4441 df-opab 4499 df-mpt 4500 df-id 4788 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-1st 6774 df-2nd 6775 df-undef 6992 df-poset 15422 df-plt 15434 df-lub 15450 df-glb 15451 df-join 15452 df-meet 15453 df-p0 15515 df-p1 15516 df-lat 15522 df-clat 15584 df-oposet 33848 df-ol 33850 df-oml 33851 df-covers 33938 df-ats 33939 df-atl 33970 df-cvlat 33994 df-hlat 34023 df-llines 34169 df-lplanes 34170 df-lvols 34171 df-lines 34172 df-psubsp 34174 df-pmap 34175 df-padd 34467 df-lhyp 34659

This theorem is referenced by: cdleme32f 35117

W3C validator