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 35873

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 1116	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
2	1	pm2.24d 143	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
3		simp11l 1106	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
4		hllat 34790	. . . . . 6
5	3, 4	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
6		simp21l 1112	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
7		simp11r 1107	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
8		cdleme32.b	. . . . . . 7
9		cdleme32.h	. . . . . . 7
10	8, 9	lhpbase 35424	. . . . . 6
11	7, 10	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
12		cdleme32.l	. . . . . 6
13		cdleme32.m	. . . . . 6 $./\$
14	8, 12, 13	latleeqm1 15578	. . . . 5 $/\$ $/\$ $./\$
15	5, 6, 11, 14	syl3anc 1227	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
16	8, 13	latmcl 15551	. . . . . . 7 $/\$ $/\$ $./\$
17	5, 6, 11, 16	syl3anc 1227	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
18		simp21r 1113	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
19	8, 13	latmcl 15551	. . . . . . 7 $/\$ $/\$ $./\$
20	5, 18, 11, 19	syl3anc 1227	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
21		simp11 1025	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
22		simp12 1026	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
23		simp13 1027	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
24		simp31 1031	. . . . . . . 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 35794	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	21, 22, 23, 24, 1, 33	syl122anc 1236	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
35	8, 25	latjcl 15550	. . . . . . 7 $/\$ $/\$ $./\$ $.\/$ $./\$
36	5, 34, 20, 35	syl3anc 1227	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
37		simp33 1033	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
38	8, 12, 13	latmlem1 15580	. . . . . . . 8 $/\$ $/\$ $/\$ $./\$ $./\$
39	5, 6, 18, 11, 38	syl13anc 1229	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $./\$
40	37, 39	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $./\$
41	8, 12, 25	latlej2 15560	. . . . . . 7 $/\$ $/\$ $./\$ $./\$ $.\/$ $./\$
42	5, 34, 20, 41	syl3anc 1227	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
43	8, 12, 5, 17, 20, 36, 40, 42	lattrd 15557	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
44		breq1 4436	. . . . 5 $./\$ $./\$ $.\/$ $./\$ $.\/$ $./\$
45	43, 44	syl5ibcom 220	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
46	15, 45	sylbid 215	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
47		simp22 1029	. . . 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 35821	. . 3 $/\$ $/\$
53	6, 47, 52	syl2anc 661	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
54		simp1 995	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		simp23 1030	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
56		simp32 1032	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
57		cdleme32.o	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $./\$
58	8, 12, 25, 13, 26, 9, 27, 28, 29, 30, 31, 32, 57, 51	cdleme32a 35869	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
59	54, 18, 55, 24, 56, 58	syl122anc 1236	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
60	50, 53, 59	3brtr4d 4463	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1381

wcel 1802

wne 2636

wral 2791

cif 3922 class class class wbr 4433

cmpt 4491

cfv 5574

crio 6237 (class class class)co 6277

cbs 14504

cple 14576

cjn 15442

cmee 15443

clat 15544

catm 34690

chlt 34777

clh 35410

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-rep 4544 ax-sep 4554 ax-nul 4562 ax-pow 4611 ax-pr 4672 ax-un 6573 ax-riotaBAD 34386

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3418 df-dif 3461 df-un 3463 df-in 3465 df-ss 3472 df-nul 3768 df-if 3923 df-pw 3995 df-sn 4011 df-pr 4013 df-op 4017 df-uni 4231 df-iun 4313 df-iin 4314 df-br 4434 df-opab 4492 df-mpt 4493 df-id 4781 df-xp 4991 df-rel 4992 df-cnv 4993 df-co 4994 df-dm 4995 df-rn 4996 df-res 4997 df-ima 4998 df-iota 5537 df-fun 5576 df-fn 5577 df-f 5578 df-f1 5579 df-fo 5580 df-f1o 5581 df-fv 5582 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-1st 6781 df-2nd 6782 df-undef 7000 df-preset 15426 df-poset 15444 df-plt 15457 df-lub 15473 df-glb 15474 df-join 15475 df-meet 15476 df-p0 15538 df-p1 15539 df-lat 15545 df-clat 15607 df-oposet 34603 df-ol 34605 df-oml 34606 df-covers 34693 df-ats 34694 df-atl 34725 df-cvlat 34749 df-hlat 34778 df-llines 34924 df-lplanes 34925 df-lvols 34926 df-lines 34927 df-psubsp 34929 df-pmap 34930 df-padd 35222 df-lhyp 35414

This theorem is referenced by: cdleme32f 35874

W3C validator