cdleme39n - Mathbox for Norm Megill

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

Theorem cdleme39n 34002

Description: Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on

$.\/$

line. TODO: FIX COMMENT.

serve as f(t), f(u), f_t(

), f_t(

). Put hypotheses of cdleme38n 34000 in convention of cdleme32sn1awN 33968. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.)

**Hypotheses**
Ref	Expression
cdleme39.l
cdleme39.j	$.\/$
cdleme39.m	$./\$
cdleme39.a
cdleme39.h
cdleme39.u	$.\/$ $./\$
cdleme39.e	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme39.g	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme39.y	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme39.z	$.\/$ $./\$ $.\/$ $.\/$ $./\$

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

**Proof of Theorem cdleme39n**
Step	Hyp	Ref	Expression
1		cdleme39.l	. . 3
2		cdleme39.j	. . 3 $.\/$
3		cdleme39.m	. . 3 $./\$
4		cdleme39.a	. . 3
5		cdleme39.h	. . 3
6		cdleme39.u	. . 3 $.\/$ $./\$
7		cdleme39.e	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$
8		cdleme39.y	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$
9		eqid 2422	. . 3 $.\/$ $./\$ $.\/$ $./\$
10		eqid 2422	. . 3 $.\/$ $./\$ $.\/$ $./\$
11		eqid 2422	. . 3 $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
12		eqid 2422	. . 3 $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	cdleme38n 34000	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
14		simp11 1035	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
15		simp12l 1118	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
16		simp13l 1120	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
17		simp22l 1124	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
18		simp22r 1125	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
19		simp311 1152	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
20		simp32l 1130	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
21		cdleme39.g	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
22	1, 2, 3, 4, 5, 6, 7, 21, 9	cdleme39a 34001	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
23	14, 15, 16, 17, 18, 19, 20, 22	syl322anc 1292	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
24		simp23l 1126	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
25		simp23r 1127	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		simp312 1153	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
27		simp33l 1132	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
28		cdleme39.z	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
29	1, 2, 3, 4, 5, 6, 8, 28, 10	cdleme39a 34001	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
30	14, 15, 16, 24, 25, 26, 27, 29	syl322anc 1292	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
31	13, 23, 30	3netr4d 2725	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872

wne 2614 class class class wbr 4423

cfv 5601 (class class class)co 6305

cple 15196

cjn 16188

cmee 16189

catm 32798

chlt 32885

clh 33518

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-ral 2776 df-rex 2777 df-reu 2778 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-op 4005 df-uni 4220 df-iun 4301 df-iin 4302 df-br 4424 df-opab 4483 df-mpt 4484 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-1st 6807 df-2nd 6808 df-preset 16172 df-poset 16190 df-plt 16203 df-lub 16219 df-glb 16220 df-join 16221 df-meet 16222 df-p0 16284 df-p1 16285 df-lat 16291 df-clat 16353 df-oposet 32711 df-ol 32713 df-oml 32714 df-covers 32801 df-ats 32802 df-atl 32833 df-cvlat 32857 df-hlat 32886 df-llines 33032 df-lplanes 33033 df-lvols 33034 df-lines 33035 df-psubsp 33037 df-pmap 33038 df-padd 33330 df-lhyp 33522

This theorem is referenced by: cdleme40m 34003

W3C validator