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 33461

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 997	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
2		simp23 1032	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
3		simp32l 1122	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
4		simp33l 1124	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
5		simp21 1030	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
6		simp32r 1123	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
7		simp33r 1125	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
8		simp31r 1121	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
9	6, 7, 8	3jca 1177	. . 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 2402	. . . 4 $.\/$ $./\$ $.\/$ $./\$
19		eqid 2402	. . . 4 $.\/$ $./\$ $.\/$ $./\$
20		eqid 2402	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
21		eqid 2402	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
22	10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21	cdleme21k 33337	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
23	1, 2, 3, 4, 5, 9, 22	syl132anc 1248	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
24		simp11 1027	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		simp12l 1110	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		simp13l 1112	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
27	10, 11, 12, 13, 14, 15	cdleme4 33236	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
28	24, 25, 26, 2, 8, 27	syl131anc 1243	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
29		cdleme37.v	. . . . . . 7 $.\/$ $./\$
30	10, 11, 12, 13, 14, 15, 16	cdleme2 33226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
31	24, 25, 26, 3, 30	syl13anc 1232	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
32	29, 31	syl5eq 2455	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
33	32	oveq2d 6293	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
34	28, 33	eqtr4d 2446	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
35		simp11l 1108	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
36		simp23l 1118	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
37	3	simpld 457	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
38	11, 13	hlatjcom 32365	. . . . . . 7 $/\$ $/\$ $.\/$ $.\/$
39	35, 36, 37, 38	syl3anc 1230	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
40	39	oveq1d 6292	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$
41	40	oveq2d 6293	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
42	34, 41	oveq12d 6295	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
43		cdleme37.c	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$
44	42, 43	syl6reqr 2462	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
45		cdleme37.x	. . . . . . 7 $.\/$ $./\$
46	10, 11, 12, 13, 14, 15, 17	cdleme2 33226	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
47	24, 25, 26, 4, 46	syl13anc 1232	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
48	45, 47	syl5eq 2455	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
49	48	oveq2d 6293	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
50	28, 49	eqtr4d 2446	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
51	4	simpld 457	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
52	11, 13	hlatjcom 32365	. . . . . . 7 $/\$ $/\$ $.\/$ $.\/$
53	35, 36, 51, 52	syl3anc 1230	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
54	53	oveq1d 6292	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$
55	54	oveq2d 6293	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
56	50, 55	oveq12d 6295	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
57		cdleme37.g	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$
58	56, 57	syl6reqr 2462	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
59	23, 44, 58	3eqtr4d 2453	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wne 2598 class class class wbr 4394

cfv 5568 (class class class)co 6277

cple 14914

cjn 15895

cmee 15896

catm 32261

chlt 32348

clh 32981

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6573

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-ral 2758 df-rex 2759 df-reu 2760 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-op 3978 df-uni 4191 df-iun 4272 df-iin 4273 df-br 4395 df-opab 4453 df-mpt 4454 df-id 4737 df-xp 4828 df-rel 4829 df-cnv 4830 df-co 4831 df-dm 4832 df-rn 4833 df-res 4834 df-ima 4835 df-iota 5532 df-fun 5570 df-fn 5571 df-f 5572 df-f1 5573 df-fo 5574 df-f1o 5575 df-fv 5576 df-riota 6239 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-1st 6783 df-2nd 6784 df-preset 15879 df-poset 15897 df-plt 15910 df-lub 15926 df-glb 15927 df-join 15928 df-meet 15929 df-p0 15991 df-p1 15992 df-lat 15998 df-clat 16060 df-oposet 32174 df-ol 32176 df-oml 32177 df-covers 32264 df-ats 32265 df-atl 32296 df-cvlat 32320 df-hlat 32349 df-llines 32495 df-lplanes 32496 df-lvols 32497 df-lines 32498 df-psubsp 32500 df-pmap 32501 df-padd 32793 df-lhyp 32985

This theorem is referenced by: cdleme38m 33462

W3C validator