cdleme38n - Mathbox for Norm Megill

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

Theorem cdleme38n 34075

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

$.\/$

line. TODO: FIX COMMENT. TODO shorter if proved directly from cdleme36m 34072 and cdleme37m 34073? (Contributed by NM, 14-Mar-2013.)

**Hypotheses**
Ref	Expression
cdleme38.l
cdleme38.j	$.\/$
cdleme38.m	$./\$
cdleme38.a
cdleme38.h
cdleme38.u	$.\/$ $./\$
cdleme38.e	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme38.d	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme38.v	$.\/$ $./\$
cdleme38.x	$.\/$ $./\$
cdleme38.f	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme38.g	$.\/$ $./\$ $.\/$ $.\/$ $./\$

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

**Proof of Theorem cdleme38n**
Step	Hyp	Ref	Expression
1		simp313 1163	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
2		simpl1 1017	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
3		simpl21 1092	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
4		simpl22 1093	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
5		simpl23 1094	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
6		simp311 1161	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
7	6	adantr 471	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
8		simp312 1162	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
9	8	adantr 471	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
10		simpr 467	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
11	7, 9, 10	3jca 1194	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
12		simpl32 1096	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
13		simpl33 1097	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
14		cdleme38.l	. . . . . 6
15		cdleme38.j	. . . . . 6 $.\/$
16		cdleme38.m	. . . . . 6 $./\$
17		cdleme38.a	. . . . . 6
18		cdleme38.h	. . . . . 6
19		cdleme38.u	. . . . . 6 $.\/$ $./\$
20		cdleme38.e	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
21		cdleme38.d	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
22		cdleme38.v	. . . . . 6 $.\/$ $./\$
23		cdleme38.x	. . . . . 6 $.\/$ $./\$
24		cdleme38.f	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
25		cdleme38.g	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
26	14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25	cdleme38m 34074	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
27	2, 3, 4, 5, 11, 12, 13, 26	syl133anc 1299	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
28	27	ex 440	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
29	28	necon3d 2656	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
30	1, 29	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 375 $/\$ w3a 991

wceq 1454

wcel 1897

wne 2632 class class class wbr 4415

cfv 5600 (class class class)co 6314

cple 15245

cjn 16237

cmee 16238

catm 32873

chlt 32960

clh 33593

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-rep 4528 ax-sep 4538 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6609

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-reu 2755 df-rab 2757 df-v 3058 df-sbc 3279 df-csb 3375 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-pw 3964 df-sn 3980 df-pr 3982 df-op 3986 df-uni 4212 df-iun 4293 df-iin 4294 df-br 4416 df-opab 4475 df-mpt 4476 df-id 4767 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 df-riota 6276 df-ov 6317 df-oprab 6318 df-mpt2 6319 df-1st 6819 df-2nd 6820 df-preset 16221 df-poset 16239 df-plt 16252 df-lub 16268 df-glb 16269 df-join 16270 df-meet 16271 df-p0 16333 df-p1 16334 df-lat 16340 df-clat 16402 df-oposet 32786 df-ol 32788 df-oml 32789 df-covers 32876 df-ats 32877 df-atl 32908 df-cvlat 32932 df-hlat 32961 df-llines 33107 df-lplanes 33108 df-lvols 33109 df-lines 33110 df-psubsp 33112 df-pmap 33113 df-padd 33405 df-lhyp 33597

This theorem is referenced by: cdleme39n 34077

W3C validator