cdleme38n - Mathbox for Norm Megill

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

Theorem cdleme38n 33937

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 33934 and cdleme37m 33935? (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 1154	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
2		simpl1 1008	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
3		simpl21 1083	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
4		simpl22 1084	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
5		simpl23 1085	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
6		simp311 1152	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
7	6	adantr 466	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
8		simp312 1153	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
9	8	adantr 466	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
10		simpr 462	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
11	7, 9, 10	3jca 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
12		simpl32 1087	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
13		simpl33 1088	. . . . 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 33936	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
27	2, 3, 4, 5, 11, 12, 13, 26	syl133anc 1287	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
28	27	ex 435	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
29	28	necon3d 2616	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
30	1, 29	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1437

wcel 1872

wne 2593 class class class wbr 4359

cfv 5537 (class class class)co 6242

cple 15133

cjn 16125

cmee 16126

catm 32735

chlt 32822

clh 33455

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 2058 ax-ext 2402 ax-rep 4472 ax-sep 4482 ax-nul 4491 ax-pow 4538 ax-pr 4596 ax-un 6534

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 2274 df-mo 2275 df-clab 2409 df-cleq 2415 df-clel 2418 df-nfc 2552 df-ne 2595 df-ral 2713 df-rex 2714 df-reu 2715 df-rab 2717 df-v 3018 df-sbc 3236 df-csb 3332 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3698 df-if 3848 df-pw 3919 df-sn 3935 df-pr 3937 df-op 3941 df-uni 4156 df-iun 4237 df-iin 4238 df-br 4360 df-opab 4419 df-mpt 4420 df-id 4704 df-xp 4795 df-rel 4796 df-cnv 4797 df-co 4798 df-dm 4799 df-rn 4800 df-res 4801 df-ima 4802 df-iota 5501 df-fun 5539 df-fn 5540 df-f 5541 df-f1 5542 df-fo 5543 df-f1o 5544 df-fv 5545 df-riota 6204 df-ov 6245 df-oprab 6246 df-mpt2 6247 df-1st 6744 df-2nd 6745 df-preset 16109 df-poset 16127 df-plt 16140 df-lub 16156 df-glb 16157 df-join 16158 df-meet 16159 df-p0 16221 df-p1 16222 df-lat 16228 df-clat 16290 df-oposet 32648 df-ol 32650 df-oml 32651 df-covers 32738 df-ats 32739 df-atl 32770 df-cvlat 32794 df-hlat 32823 df-llines 32969 df-lplanes 32970 df-lvols 32971 df-lines 32972 df-psubsp 32974 df-pmap 32975 df-padd 33267 df-lhyp 33459

This theorem is referenced by: cdleme39n 33939

W3C validator