cdleme16e - Mathbox for Norm Megill

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

Theorem cdleme16e 29844

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 1066	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		hllat 28926	. . . . 5
3	1, 2	syl 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4		simp21l 1072	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
5		simp22l 1074	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
6		eqid 2283	. . . . . 6
7		cdleme12.j	. . . . . 6 $.\/$
8		cdleme12.a	. . . . . 6
9	6, 7, 8	hlatjcl 28929	. . . . 5 $/\$ $/\$ $.\/$
10	1, 4, 5, 9	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
11		simp11 985	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
12		simp12 986	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
13		simp13 987	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
14		simp21 988	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
15		simp23l 1076	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
16		simp31 991	. . . . . 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 29798	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	11, 12, 13, 14, 15, 16, 22	syl132anc 1200	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
24		simp22 989	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
25		simp32 992	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
26		cdleme12.g	. . . . . . 7 $.\/$ $./\$ $.\/$ $.\/$ $./\$
27	17, 7, 18, 8, 19, 20, 26	cdleme3fa 29798	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
28	11, 12, 13, 24, 15, 25, 27	syl132anc 1200	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
29	6, 7, 8	hlatjcl 28929	. . . . 5 $/\$ $/\$ $.\/$
30	1, 23, 28, 29	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
31	6, 17, 18	latmle1 14182	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
32	3, 10, 30, 31	syl3anc 1182	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
33	17, 7, 18, 8, 19, 20, 21, 26	cdleme15 29840	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
34	6, 18	latmcl 14157	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
35	3, 10, 30, 34	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
36		simp11r 1067	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
37	6, 19	lhpbase 29560	. . . . 5
38	36, 37	syl 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
39	6, 17, 18	latlem12 14184	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
40	3, 35, 10, 38, 39	syl13anc 1184	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
41	32, 33, 40	mpbi2and 887	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
42		hlatl 28923	. . . 4
43	1, 42	syl 15	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
44	17, 7, 18, 8, 19, 20, 21, 26	cdleme16d 29843	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
45		simp21r 1073	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
46		simp23r 1077	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
47	17, 7, 18, 8, 19	lhpat 29605	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
48	1, 36, 4, 45, 5, 46, 47	syl222anc 1198	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
49	17, 8	atcmp 28874	. . 3 $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
50	43, 44, 48, 49	syl3anc 1182	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
51	41, 50	mpbid 201	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 176 $/\$ wa 358 $/\$ w3a 934

wceq 1623

wcel 1684

wne 2446 class class class wbr 4023

cfv 5255 (class class class)co 5858

cbs 13148

cple 13215

cjn 14078

cmee 14079

clat 14151

catm 28826

cal 28827

chlt 28913

clh 29546

This theorem is referenced by: cdleme16g 29846

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1533 ax-5 1544 ax-17 1603 ax-9 1635 ax-8 1643 ax-13 1686 ax-14 1688 ax-6 1703 ax-7 1708 ax-11 1715 ax-12 1866 ax-ext 2264 ax-rep 4131 ax-sep 4141 ax-nul 4149 ax-pow 4188 ax-pr 4214 ax-un 4512

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-tru 1310 df-ex 1529 df-nf 1532 df-sb 1630 df-eu 2147 df-mo 2148 df-clab 2270 df-cleq 2276 df-clel 2279 df-nfc 2408 df-ne 2448 df-nel 2449 df-ral 2548 df-rex 2549 df-reu 2550 df-rab 2552 df-v 2790 df-sbc 2992 df-csb 3082 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3456 df-if 3566 df-pw 3627 df-sn 3646 df-pr 3647 df-op 3649 df-uni 3828 df-iun 3907 df-iin 3908 df-br 4024 df-opab 4078 df-mpt 4079 df-id 4309 df-xp 4695 df-rel 4696 df-cnv 4697 df-co 4698 df-dm 4699 df-rn 4700 df-res 4701 df-ima 4702 df-iota 5219 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-ov 5861 df-oprab 5862 df-mpt2 5863 df-1st 6122 df-2nd 6123 df-undef 6298 df-riota 6304 df-poset 14080 df-plt 14092 df-lub 14108 df-glb 14109 df-join 14110 df-meet 14111 df-p0 14145 df-p1 14146 df-lat 14152 df-clat 14214 df-oposet 28739 df-ol 28741 df-oml 28742 df-covers 28829 df-ats 28830 df-atl 28861 df-cvlat 28885 df-hlat 28914 df-llines 29060 df-lplanes 29061 df-lvols 29062 df-lines 29063 df-psubsp 29065 df-pmap 29066 df-padd 29358 df-lhyp 29550

W3C validator