cdleme16e - Mathbox for Norm Megill

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

Theorem cdleme16e 31079

Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence.

and

represent f(s) and f(t) respectively. We show, in their notation, (s $\/$ t) $/\$ (f(s) $\/$ f(t))=(s $\/$ t) $/\$ w. (Contributed by NM, 11-Oct-2012.)

**Hypotheses**
Ref	Expression
cdleme12.l
cdleme12.j	$.\/$
cdleme12.m	$./\$
cdleme12.a
cdleme12.h
cdleme12.u	$.\/$ $./\$
cdleme12.f	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme12.g	$.\/$ $./\$ $.\/$ $.\/$ $./\$

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

**Proof of Theorem cdleme16e**
Step	Hyp	Ref	Expression
1		simp11l 1068	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		hllat 30161	. . . . 5
3	1, 2	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4		simp21l 1074	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
5		simp22l 1076	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
6		eqid 2436	. . . . . 6
7		cdleme12.j	. . . . . 6 $.\/$
8		cdleme12.a	. . . . . 6
9	6, 7, 8	hlatjcl 30164	. . . . 5 $/\$ $/\$ $.\/$
10	1, 4, 5, 9	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
11		simp11 987	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
12		simp12 988	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
13		simp13 989	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
14		simp21 990	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
15		simp23l 1078	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
16		simp31 993	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
17		cdleme12.l	. . . . . . 7
18		cdleme12.m	. . . . . . 7 $./\$
19		cdleme12.h	. . . . . . 7
20		cdleme12.u	. . . . . . 7 $.\/$ $./\$
21		cdleme12.f	. . . . . . 7 $.\/$ $./\$ $.\/$ $.\/$ $./\$
22	17, 7, 18, 8, 19, 20, 21	cdleme3fa 31033	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	11, 12, 13, 14, 15, 16, 22	syl132anc 1202	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
24		simp22 991	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
25		simp32 994	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
26		cdleme12.g	. . . . . . 7 $.\/$ $./\$ $.\/$ $.\/$ $./\$
27	17, 7, 18, 8, 19, 20, 26	cdleme3fa 31033	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
28	11, 12, 13, 24, 15, 25, 27	syl132anc 1202	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
29	6, 7, 8	hlatjcl 30164	. . . . 5 $/\$ $/\$ $.\/$
30	1, 23, 28, 29	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
31	6, 17, 18	latmle1 14505	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
32	3, 10, 30, 31	syl3anc 1184	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
33	17, 7, 18, 8, 19, 20, 21, 26	cdleme15 31075	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
34	6, 18	latmcl 14480	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
35	3, 10, 30, 34	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
36		simp11r 1069	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
37	6, 19	lhpbase 30795	. . . . 5
38	36, 37	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
39	6, 17, 18	latlem12 14507	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
40	3, 35, 10, 38, 39	syl13anc 1186	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
41	32, 33, 40	mpbi2and 888	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
42		hlatl 30158	. . . 4
43	1, 42	syl 16	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
44	17, 7, 18, 8, 19, 20, 21, 26	cdleme16d 31078	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
45		simp21r 1075	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
46		simp23r 1079	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
47	17, 7, 18, 8, 19	lhpat 30840	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
48	1, 36, 4, 45, 5, 46, 47	syl222anc 1200	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
49	17, 8	atcmp 30109	. . 3 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
50	43, 44, 48, 49	syl3anc 1184	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
51	41, 50	mpbid 202	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1652

wcel 1725

wne 2599 class class class wbr 4212

cfv 5454 (class class class)co 6081

cbs 13469

cple 13536

cjn 14401

cmee 14402

clat 14474

catm 30061

cal 30062

chlt 30148

clh 30781

This theorem is referenced by: cdleme16g 31081

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1555 ax-5 1566 ax-17 1626 ax-9 1666 ax-8 1687 ax-13 1727 ax-14 1729 ax-6 1744 ax-7 1749 ax-11 1761 ax-12 1950 ax-ext 2417 ax-rep 4320 ax-sep 4330 ax-nul 4338 ax-pow 4377 ax-pr 4403 ax-un 4701

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1328 df-ex 1551 df-nf 1554 df-sb 1659 df-eu 2285 df-mo 2286 df-clab 2423 df-cleq 2429 df-clel 2432 df-nfc 2561 df-ne 2601 df-nel 2602 df-ral 2710 df-rex 2711 df-reu 2712 df-rab 2714 df-v 2958 df-sbc 3162 df-csb 3252 df-dif 3323 df-un 3325 df-in 3327 df-ss 3334 df-nul 3629 df-if 3740 df-pw 3801 df-sn 3820 df-pr 3821 df-op 3823 df-uni 4016 df-iun 4095 df-iin 4096 df-br 4213 df-opab 4267 df-mpt 4268 df-id 4498 df-xp 4884 df-rel 4885 df-cnv 4886 df-co 4887 df-dm 4888 df-rn 4889 df-res 4890 df-ima 4891 df-iota 5418 df-fun 5456 df-fn 5457 df-f 5458 df-f1 5459 df-fo 5460 df-f1o 5461 df-fv 5462 df-ov 6084 df-oprab 6085 df-mpt2 6086 df-1st 6349 df-2nd 6350 df-undef 6543 df-riota 6549 df-poset 14403 df-plt 14415 df-lub 14431 df-glb 14432 df-join 14433 df-meet 14434 df-p0 14468 df-p1 14469 df-lat 14475 df-clat 14537 df-oposet 29974 df-ol 29976 df-oml 29977 df-covers 30064 df-ats 30065 df-atl 30096 df-cvlat 30120 df-hlat 30149 df-llines 30295 df-lplanes 30296 df-lvols 30297 df-lines 30298 df-psubsp 30300 df-pmap 30301 df-padd 30593 df-lhyp 30785

W3C validator