cdleme37m - Mathbox for Norm Megill

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

Theorem cdleme37m 34469

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

$.\/$

line. TODO: FIX COMMENT (Contributed by NM, 13-Mar-2013.)

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

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

**Proof of Theorem cdleme37m**
Step	Hyp	Ref	Expression
1		simp1 988	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
2		simp23 1023	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
3		simp32l 1113	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
4		simp33l 1115	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
5		simp21 1021	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
6		simp32r 1114	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
7		simp33r 1116	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
8		simp31r 1112	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
9	6, 7, 8	3jca 1168	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
10		cdleme37.l	. . . 4
11		cdleme37.j	. . . 4 $.\/$
12		cdleme37.m	. . . 4 $./\$
13		cdleme37.a	. . . 4
14		cdleme37.h	. . . 4
15		cdleme37.u	. . . 4 $.\/$ $./\$
16		cdleme37.e	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
17		cdleme37.d	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
18		eqid 2454	. . . 4 $.\/$ $./\$ $.\/$ $./\$
19		eqid 2454	. . . 4 $.\/$ $./\$ $.\/$ $./\$
20		eqid 2454	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
21		eqid 2454	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
22	10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21	cdleme21k 34345	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
23	1, 2, 3, 4, 5, 9, 22	syl132anc 1237	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
24		simp11 1018	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		simp12l 1101	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		simp13l 1103	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
27	10, 11, 12, 13, 14, 15	cdleme4 34245	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
28	24, 25, 26, 2, 8, 27	syl131anc 1232	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
29		cdleme37.v	. . . . . . 7 $.\/$ $./\$
30	10, 11, 12, 13, 14, 15, 16	cdleme2 34235	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
31	24, 25, 26, 3, 30	syl13anc 1221	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
32	29, 31	syl5eq 2507	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
33	32	oveq2d 6219	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
34	28, 33	eqtr4d 2498	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
35		simp11l 1099	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
36		simp23l 1109	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
37	3	simpld 459	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
38	11, 13	hlatjcom 33375	. . . . . . 7 $/\$ $/\$ $.\/$ $.\/$
39	35, 36, 37, 38	syl3anc 1219	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
40	39	oveq1d 6218	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$
41	40	oveq2d 6219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
42	34, 41	oveq12d 6221	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
43		cdleme37.c	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$
44	42, 43	syl6reqr 2514	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
45		cdleme37.x	. . . . . . 7 $.\/$ $./\$
46	10, 11, 12, 13, 14, 15, 17	cdleme2 34235	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
47	24, 25, 26, 4, 46	syl13anc 1221	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
48	45, 47	syl5eq 2507	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
49	48	oveq2d 6219	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
50	28, 49	eqtr4d 2498	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
51	4	simpld 459	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
52	11, 13	hlatjcom 33375	. . . . . . 7 $/\$ $/\$ $.\/$ $.\/$
53	35, 36, 51, 52	syl3anc 1219	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
54	53	oveq1d 6218	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$
55	54	oveq2d 6219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
56	50, 55	oveq12d 6221	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
57		cdleme37.g	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$
58	56, 57	syl6reqr 2514	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
59	23, 44, 58	3eqtr4d 2505	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1370

wcel 1758

wne 2648 class class class wbr 4403

cfv 5529 (class class class)co 6203

cple 14368

cjn 15237

cmee 15238

catm 33271

chlt 33358

clh 33991

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 1955 ax-ext 2432 ax-rep 4514 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485

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 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-op 3995 df-uni 4203 df-iun 4284 df-iin 4285 df-br 4404 df-opab 4462 df-mpt 4463 df-id 4747 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-riota 6164 df-ov 6206 df-oprab 6207 df-mpt2 6208 df-1st 6690 df-2nd 6691 df-poset 15239 df-plt 15251 df-lub 15267 df-glb 15268 df-join 15269 df-meet 15270 df-p0 15332 df-p1 15333 df-lat 15339 df-clat 15401 df-oposet 33184 df-ol 33186 df-oml 33187 df-covers 33274 df-ats 33275 df-atl 33306 df-cvlat 33330 df-hlat 33359 df-llines 33505 df-lplanes 33506 df-lvols 33507 df-lines 33508 df-psubsp 33510 df-pmap 33511 df-padd 33803 df-lhyp 33995

This theorem is referenced by: cdleme38m 34470

W3C validator