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 34418

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 34416 in convention of cdleme32sn1awN 34384. 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 2451	. . 3 $.\/$ $./\$ $.\/$ $./\$
10		eqid 2451	. . 3 $.\/$ $./\$ $.\/$ $./\$
11		eqid 2451	. . 3 $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
12		eqid 2451	. . 3 $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	cdleme38n 34416	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
14		simp11 1018	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
15		simp12l 1101	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
16		simp13l 1103	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
17		simp22l 1107	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
18		simp22r 1108	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
19		simp311 1135	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
20		simp32l 1113	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
21		cdleme39.g	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
22	1, 2, 3, 4, 5, 6, 7, 21, 9	cdleme39a 34417	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
23	14, 15, 16, 17, 18, 19, 20, 22	syl322anc 1247	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
24		simp23l 1109	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
25		simp23r 1110	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		simp312 1136	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
27		simp33l 1115	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
28		cdleme39.z	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
29	1, 2, 3, 4, 5, 6, 8, 28, 10	cdleme39a 34417	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
30	14, 15, 16, 24, 25, 26, 27, 29	syl322anc 1247	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
31	13, 23, 30	3netr4d 2753	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1370

wcel 1758

wne 2644 class class class wbr 4392

cfv 5518 (class class class)co 6192

cple 14349

cjn 15218

cmee 15219

catm 33216

chlt 33303

clh 33936

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4503 ax-sep 4513 ax-nul 4521 ax-pow 4570 ax-pr 4631 ax-un 6474

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rex 2801 df-reu 2802 df-rab 2804 df-v 3072 df-sbc 3287 df-csb 3389 df-dif 3431 df-un 3433 df-in 3435 df-ss 3442 df-nul 3738 df-if 3892 df-pw 3962 df-sn 3978 df-pr 3980 df-op 3984 df-uni 4192 df-iun 4273 df-iin 4274 df-br 4393 df-opab 4451 df-mpt 4452 df-id 4736 df-xp 4946 df-rel 4947 df-cnv 4948 df-co 4949 df-dm 4950 df-rn 4951 df-res 4952 df-ima 4953 df-iota 5481 df-fun 5520 df-fn 5521 df-f 5522 df-f1 5523 df-fo 5524 df-f1o 5525 df-fv 5526 df-riota 6153 df-ov 6195 df-oprab 6196 df-mpt2 6197 df-1st 6679 df-2nd 6680 df-poset 15220 df-plt 15232 df-lub 15248 df-glb 15249 df-join 15250 df-meet 15251 df-p0 15313 df-p1 15314 df-lat 15320 df-clat 15382 df-oposet 33129 df-ol 33131 df-oml 33132 df-covers 33219 df-ats 33220 df-atl 33251 df-cvlat 33275 df-hlat 33304 df-llines 33450 df-lplanes 33451 df-lvols 33452 df-lines 33453 df-psubsp 33455 df-pmap 33456 df-padd 33748 df-lhyp 33940

This theorem is referenced by: cdleme40m 34419

W3C validator