cdleme26e - Mathbox for Norm Megill

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

Theorem cdleme26e 33391

Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115.

represent f(z), f_z(s), f_z(t) respectively. When t $\/$ v = p $\/$ q, f_z(s)

f_z(t) $\/$ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)

**Hypotheses**
Ref	Expression
cdleme26.b
cdleme26.l
cdleme26.j	$.\/$
cdleme26.m	$./\$
cdleme26.a
cdleme26.h
cdleme26e.u	$.\/$ $./\$
cdleme26e.f	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme26e.n	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme26e.o	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme26e.i	$/\$ $.\/$
cdleme26e.e	$/\$ $.\/$

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

Distinct variable groups:

, $.\/$ ,

, $./\$ ,

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem cdleme26e**
Step	Hyp	Ref	Expression
1		simp11 1029	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$
2		simp12 1030	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$
3		simp13 1031	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$
4		simp21l 1116	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
5		simp22l 1118	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
6	4, 5	jca 532	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$
7		simp23 1034	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$
8		simp311 1146	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
9		simp32l 1124	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
10	8, 9	jca 532	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
11		simp33 1037	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$
12		cdleme26.l	. . . 4
13		cdleme26.j	. . . 4 $.\/$
14		cdleme26.m	. . . 4 $./\$
15		cdleme26.a	. . . 4
16		cdleme26.h	. . . 4
17		cdleme26e.u	. . . 4 $.\/$ $./\$
18		cdleme26e.f	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
19		cdleme26e.n	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
20		cdleme26e.o	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
21	12, 13, 14, 15, 16, 17, 18, 19, 20	cdleme22e 33376	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$
22	1, 2, 3, 6, 7, 10, 11, 21	syl133anc 1255	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$
23		simp21r 1117	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
24		simp312 1147	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$
25		cdleme26.b	. . . . 5
26		cdleme26e.i	. . . . 5 $/\$ $.\/$
27	25, 12, 13, 14, 15, 16, 17, 18, 19, 26	cdleme25cl 33389	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
28	1, 2, 3, 4, 23, 8, 24, 27	syl322anc 1260	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
29		simp33l 1126	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
30		simp33r 1127	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
31		simp32r 1125	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$
32	30, 31	jca 532	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
33		fvex 5861	. . . . 5
34	25, 33	eqeltri 2488	. . . 4
35	34, 26	riotasv 31996	. . 3 $/\$ $/\$ $/\$ $.\/$
36	28, 29, 32, 35	syl3anc 1232	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
37		simp22r 1119	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
38		simp313 1148	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$
39		cdleme26e.e	. . . . . 6 $/\$ $.\/$
40	25, 12, 13, 14, 15, 16, 17, 18, 20, 39	cdleme25cl 33389	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
41	1, 2, 3, 5, 37, 8, 38, 40	syl322anc 1260	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
42	34, 39	riotasv 31996	. . . 4 $/\$ $/\$ $/\$ $.\/$
43	41, 29, 32, 42	syl3anc 1232	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$
44	43	oveq1d 6295	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
45	22, 36, 44	3brtr4d 4427	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1407

wcel 1844

wne 2600

wral 2756

cvv 3061 class class class wbr 4397

cfv 5571

crio 6241 (class class class)co 6280

cbs 14843

cple 14918

cjn 15899

cmee 15900

catm 32294

chlt 32381

clh 33014

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1641 ax-4 1654 ax-5 1727 ax-6 1773 ax-7 1816 ax-8 1846 ax-9 1848 ax-10 1863 ax-11 1868 ax-12 1880 ax-13 2028 ax-ext 2382 ax-rep 4509 ax-sep 4519 ax-nul 4527 ax-pow 4574 ax-pr 4632 ax-un 6576 ax-riotaBAD 31990

This theorem depends on definitions: df-bi 187 df-or 370 df-an 371 df-3or 977 df-3an 978 df-tru 1410 df-ex 1636 df-nf 1640 df-sb 1766 df-eu 2244 df-mo 2245 df-clab 2390 df-cleq 2396 df-clel 2399 df-nfc 2554 df-ne 2602 df-nel 2603 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3063 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3741 df-if 3888 df-pw 3959 df-sn 3975 df-pr 3977 df-op 3981 df-uni 4194 df-iun 4275 df-iin 4276 df-br 4398 df-opab 4456 df-mpt 4457 df-id 4740 df-xp 4831 df-rel 4832 df-cnv 4833 df-co 4834 df-dm 4835 df-rn 4836 df-res 4837 df-ima 4838 df-iota 5535 df-fun 5573 df-fn 5574 df-f 5575 df-f1 5576 df-fo 5577 df-f1o 5578 df-fv 5579 df-riota 6242 df-ov 6283 df-oprab 6284 df-mpt2 6285 df-1st 6786 df-2nd 6787 df-undef 7007 df-preset 15883 df-poset 15901 df-plt 15914 df-lub 15930 df-glb 15931 df-join 15932 df-meet 15933 df-p0 15995 df-p1 15996 df-lat 16002 df-clat 16064 df-oposet 32207 df-ol 32209 df-oml 32210 df-covers 32297 df-ats 32298 df-atl 32329 df-cvlat 32353 df-hlat 32382 df-llines 32528 df-lplanes 32529 df-lvols 32530 df-lines 32531 df-psubsp 32533 df-pmap 32534 df-padd 32826 df-lhyp 33018

This theorem is referenced by: cdleme26ee 33392

W3C validator