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 34392

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 1109	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
2	1	pm2.24d 143	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
3		simp11l 1099	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
4		hllat 33311	. . . . . 6
5	3, 4	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
6		simp21l 1105	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
7		simp11r 1100	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
8		cdleme32.b	. . . . . . 7
9		cdleme32.h	. . . . . . 7
10	8, 9	lhpbase 33945	. . . . . 6
11	7, 10	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
12		cdleme32.l	. . . . . 6
13		cdleme32.m	. . . . . 6 $./\$
14	8, 12, 13	latleeqm1 15348	. . . . 5 $/\$ $/\$ $./\$
15	5, 6, 11, 14	syl3anc 1219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
16	8, 13	latmcl 15321	. . . . . . 7 $/\$ $/\$ $./\$
17	5, 6, 11, 16	syl3anc 1219	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
18		simp21r 1106	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
19	8, 13	latmcl 15321	. . . . . . 7 $/\$ $/\$ $./\$
20	5, 18, 11, 19	syl3anc 1219	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$
21		simp11 1018	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
22		simp12 1019	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
23		simp13 1020	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
24		simp31 1024	. . . . . . . 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 34313	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	21, 22, 23, 24, 1, 33	syl122anc 1228	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
35	8, 25	latjcl 15320	. . . . . . 7 $/\$ $/\$ $./\$ $.\/$ $./\$
36	5, 34, 20, 35	syl3anc 1219	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
37		simp33 1026	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
38	8, 12, 13	latmlem1 15350	. . . . . . . 8 $/\$ $/\$ $/\$ $./\$ $./\$
39	5, 6, 18, 11, 38	syl13anc 1221	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $./\$
40	37, 39	mpd 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $./\$
41	8, 12, 25	latlej2 15330	. . . . . . 7 $/\$ $/\$ $./\$ $./\$ $.\/$ $./\$
42	5, 34, 20, 41	syl3anc 1219	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
43	8, 12, 5, 17, 20, 36, 40, 42	lattrd 15327	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
44		breq1 4390	. . . . 5 $./\$ $./\$ $.\/$ $./\$ $.\/$ $./\$
45	43, 44	syl5ibcom 220	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $./\$ $.\/$ $./\$
46	15, 45	sylbid 215	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
47		simp22 1022	. . . 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 34340	. . 3 $/\$ $/\$
53	6, 47, 52	syl2anc 661	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$
54		simp1 988	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55		simp23 1023	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $/\$
56		simp32 1025	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
57		cdleme32.o	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $./\$
58	8, 12, 25, 13, 26, 9, 27, 28, 29, 30, 31, 32, 57, 51	cdleme32a 34388	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
59	54, 18, 55, 24, 56, 58	syl122anc 1228	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$
60	50, 53, 59	3brtr4d 4417	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1370

wcel 1758

wne 2642

wral 2793

cif 3886 class class class wbr 4387

cmpt 4445

cfv 5513

crio 6147 (class class class)co 6187

cbs 14273

cple 14344

cjn 15213

cmee 15214

clat 15314

catm 33211

chlt 33298

clh 33931

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4498 ax-sep 4508 ax-nul 4516 ax-pow 4565 ax-pr 4626 ax-un 6469 ax-riotaBAD 32907

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2599 df-ne 2644 df-nel 2645 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3067 df-sbc 3282 df-csb 3384 df-dif 3426 df-un 3428 df-in 3430 df-ss 3437 df-nul 3733 df-if 3887 df-pw 3957 df-sn 3973 df-pr 3975 df-op 3979 df-uni 4187 df-iun 4268 df-iin 4269 df-br 4388 df-opab 4446 df-mpt 4447 df-id 4731 df-xp 4941 df-rel 4942 df-cnv 4943 df-co 4944 df-dm 4945 df-rn 4946 df-res 4947 df-ima 4948 df-iota 5476 df-fun 5515 df-fn 5516 df-f 5517 df-f1 5518 df-fo 5519 df-f1o 5520 df-fv 5521 df-riota 6148 df-ov 6190 df-oprab 6191 df-mpt2 6192 df-1st 6674 df-2nd 6675 df-undef 6889 df-poset 15215 df-plt 15227 df-lub 15243 df-glb 15244 df-join 15245 df-meet 15246 df-p0 15308 df-p1 15309 df-lat 15315 df-clat 15377 df-oposet 33124 df-ol 33126 df-oml 33127 df-covers 33214 df-ats 33215 df-atl 33246 df-cvlat 33270 df-hlat 33299 df-llines 33445 df-lplanes 33446 df-lvols 33447 df-lines 33448 df-psubsp 33450 df-pmap 33451 df-padd 33743 df-lhyp 33935

This theorem is referenced by: cdleme32f 34393

W3C validator