cdleme22g - Mathbox for Norm Megill

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

Theorem cdleme22g 36217

Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115.

represent f(s), f(t) respectively. If s

t $\/$ v and

p $\/$ q, then f(s)

f(t) $\/$ v. (Contributed by NM, 6-Dec-2012.)

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

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

**Proof of Theorem cdleme22g**
Step	Hyp	Ref	Expression
1		simp11l 1107	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
2		hllat 35231	. . . . 5
3	1, 2	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
4		simp11 1026	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
5		simp2l 1022	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
6		simp2r 1023	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
7		simp31 1032	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
8		simp133 1133	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
9		simp132 1132	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
10		cdleme22.l	. . . . . . 7
11		cdleme22.j	. . . . . . 7 $.\/$
12		cdleme22.m	. . . . . . 7 $./\$
13		cdleme22.a	. . . . . . 7
14		cdleme22.h	. . . . . . 7
15		cdleme22g.u	. . . . . . 7 $.\/$ $./\$
16		cdleme22g.f	. . . . . . 7 $.\/$ $./\$ $.\/$ $.\/$ $./\$
17	10, 11, 12, 13, 14, 15, 16	cdleme3fa 36104	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
18	4, 5, 6, 7, 8, 9, 17	syl132anc 1246	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
19		simp12 1027	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
20		simp131 1131	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
21		cdleme22g.g	. . . . . . 7 $.\/$ $./\$ $.\/$ $.\/$ $./\$
22	10, 11, 12, 13, 14, 15, 21	cdleme3fa 36104	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23	4, 5, 6, 19, 8, 20, 22	syl132anc 1246	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
24		eqid 2457	. . . . . 6
25	24, 11, 13	hlatjcl 35234	. . . . 5 $/\$ $/\$ $.\/$
26	1, 18, 23, 25	syl3anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
27		simp11r 1108	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
28	24, 14	lhpbase 35865	. . . . 5
29	27, 28	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
30	24, 10, 12	latmle1 15833	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
31	3, 26, 29, 30	syl3anc 1228	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $./\$ $.\/$
32		simp33 1034	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
33		simp32 1033	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
34	10, 11, 12, 13, 14	cdleme22d 36212	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
35	4, 7, 19, 32, 33, 34	syl131anc 1241	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $./\$
36		simp32l 1121	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
37	8, 36	jca 532	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
38	10, 11, 12, 13, 14, 15, 16, 21	cdleme16 36153	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$
39	4, 5, 6, 7, 19, 37, 9, 20, 38	syl332anc 1259	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$
40	35, 39	eqtr2d 2499	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $./\$
41	11, 13	hlatjcom 35235	. . . 4 $/\$ $/\$ $.\/$ $.\/$
42	1, 18, 23, 41	syl3anc 1228	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
43	31, 40, 42	3brtr3d 4485	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
44		hlcvl 35227	. . . 4
45	1, 44	syl 16	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
46		simp33l 1123	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
47		simp33r 1124	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
48	10, 11, 12, 13, 14, 15, 21	cdleme3 36105	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49	4, 5, 6, 19, 8, 20, 48	syl132anc 1246	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
50		nbrne2 4474	. . . 4 $/\$
51	47, 49, 50	syl2anc 661	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
52	10, 11, 13	cvlatexch1 35204	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
53	45, 46, 18, 23, 51, 52	syl131anc 1241	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
54	43, 53	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wcel 1819

wne 2652 class class class wbr 4456

cfv 5594 (class class class)co 6296

cbs 14644

cple 14719

cjn 15700

cmee 15701

clat 15802

catm 35131

clc 35133

chlt 35218

clh 35851

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-iun 4334 df-iin 4335 df-br 4457 df-opab 4516 df-mpt 4517 df-id 4804 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-1st 6799 df-2nd 6800 df-preset 15684 df-poset 15702 df-plt 15715 df-lub 15731 df-glb 15732 df-join 15733 df-meet 15734 df-p0 15796 df-p1 15797 df-lat 15803 df-clat 15865 df-oposet 35044 df-ol 35046 df-oml 35047 df-covers 35134 df-ats 35135 df-atl 35166 df-cvlat 35190 df-hlat 35219 df-llines 35365 df-lplanes 35366 df-lvols 35367 df-lines 35368 df-psubsp 35370 df-pmap 35371 df-padd 35663 df-lhyp 35855

This theorem is referenced by: cdleme27a 36236

W3C validator