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 33498

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 33496 in convention of cdleme32sn1awN 33464. 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 2404	. . 3 $.\/$ $./\$ $.\/$ $./\$
10		eqid 2404	. . 3 $.\/$ $./\$ $.\/$ $./\$
11		eqid 2404	. . 3 $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
12		eqid 2404	. . 3 $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
13	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	cdleme38n 33496	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
14		simp11 1029	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
15		simp12l 1112	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
16		simp13l 1114	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
17		simp22l 1118	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
18		simp22r 1119	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
19		simp311 1146	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
20		simp32l 1124	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
21		cdleme39.g	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
22	1, 2, 3, 4, 5, 6, 7, 21, 9	cdleme39a 33497	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
23	14, 15, 16, 17, 18, 19, 20, 22	syl322anc 1260	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
24		simp23l 1120	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
25		simp23r 1121	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		simp312 1147	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
27		simp33l 1126	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
28		cdleme39.z	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$
29	1, 2, 3, 4, 5, 6, 8, 28, 10	cdleme39a 33497	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
30	14, 15, 16, 24, 25, 26, 27, 29	syl322anc 1260	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $./\$ $.\/$ $.\/$ $./\$
31	13, 23, 30	3netr4d 2710	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wceq 1407

wcel 1844

wne 2600 class class class wbr 4397

cfv 5571 (class class class)co 6280

cple 14918

cjn 15899

cmee 15900

catm 32294

chlt 32381

clh 33014

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1641 ax-4 1654 ax-5 1727 ax-6 1773 ax-7 1816 ax-8 1846 ax-9 1848 ax-10 1863 ax-11 1868 ax-12 1880 ax-13 2028 ax-ext 2382 ax-rep 4509 ax-sep 4519 ax-nul 4527 ax-pow 4574 ax-pr 4632 ax-un 6576

This theorem depends on definitions: df-bi 187 df-or 370 df-an 371 df-3or 977 df-3an 978 df-tru 1410 df-ex 1636 df-nf 1640 df-sb 1766 df-eu 2244 df-mo 2245 df-clab 2390 df-cleq 2396 df-clel 2399 df-nfc 2554 df-ne 2602 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3063 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-nul 3741 df-if 3888 df-pw 3959 df-sn 3975 df-pr 3977 df-op 3981 df-uni 4194 df-iun 4275 df-iin 4276 df-br 4398 df-opab 4456 df-mpt 4457 df-id 4740 df-xp 4831 df-rel 4832 df-cnv 4833 df-co 4834 df-dm 4835 df-rn 4836 df-res 4837 df-ima 4838 df-iota 5535 df-fun 5573 df-fn 5574 df-f 5575 df-f1 5576 df-fo 5577 df-f1o 5578 df-fv 5579 df-riota 6242 df-ov 6283 df-oprab 6284 df-mpt2 6285 df-1st 6786 df-2nd 6787 df-preset 15883 df-poset 15901 df-plt 15914 df-lub 15930 df-glb 15931 df-join 15932 df-meet 15933 df-p0 15995 df-p1 15996 df-lat 16002 df-clat 16064 df-oposet 32207 df-ol 32209 df-oml 32210 df-covers 32297 df-ats 32298 df-atl 32329 df-cvlat 32353 df-hlat 32382 df-llines 32528 df-lplanes 32529 df-lvols 32530 df-lines 32531 df-psubsp 32533 df-pmap 32534 df-padd 32826 df-lhyp 33018

This theorem is referenced by: cdleme40m 33499

W3C validator