linethru - Mathbox for Scott Fenton

	Mathbox for Scott Fenton	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > linethru		Structured version Unicode version

Theorem linethru 30705

Description: If

is a line containing two distinct points

and

, then

is the line through

and

. Theorem 6.18 of [Schwabhauser] p. 45. (Contributed by Scott Fenton, 28-Oct-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Assertion**
Ref	Expression
linethru	LinesEE $/\$ $/\$ $/\$ Line

Proof of Theorem linethru Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ellines 30704	. . 3 LinesEE $/\$ Line
2		simpll1 1044	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
3		simpll2 1045	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
4		simpll3 1046	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
5		simplr 760	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
6		liness 30697	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ Line
7	2, 3, 4, 5, 6	syl13anc 1266	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
8		simprll 770	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
9	7, 8	sseldd 3471	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
10		simprlr 771	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
11	7, 10	sseldd 3471	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
12		simplll 766	. . . . . . . . . . . . . . . 16 Line $/\$ Line $/\$ $/\$ $/\$ Line
13	12	adantl 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line
14		simpll1 1044	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
15		simpll2 1045	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
16		simpll3 1046	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
17		simplr 760	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
18		simprrl 772	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
19		simprlr 771	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
20	19	necomd 2702	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
21		lineelsb2 30700	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
22	14, 15, 16, 17, 18, 20, 21	syl132anc 1282	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line Line
23	13, 22	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
24		linecom 30702	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ Line Line
25	14, 15, 18, 20, 24	syl13anc 1266	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
26	23, 25	eqtrd 2470	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
27		neeq2 2714	. . . . . . . . . . . . . . . . 17
28	27	anbi2d 708	. . . . . . . . . . . . . . . 16 Line $/\$ Line $/\$ Line $/\$ Line $/\$
29	28	anbi1d 709	. . . . . . . . . . . . . . 15 Line $/\$ Line $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
30	29	anbi2d 708	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
31		oveq2 6313	. . . . . . . . . . . . . . 15 Line Line
32	31	eqeq2d 2443	. . . . . . . . . . . . . 14 Line Line Line Line
33	30, 32	imbi12d 321	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
34	26, 33	mpbiri 236	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
35		simp1 1005	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simp2l 1031	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
37	35, 36, 10	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
38		simp1l1 1098	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
39		simp1l2 1099	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
40		simp1l3 1100	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
41		simp1r 1030	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
42		simp2rr 1075	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
43		simp3 1007	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
44	43	necomd 2702	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
45		lineelsb2 30700	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
46	38, 39, 40, 41, 42, 44, 45	syl132anc 1282	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line Line
47	37, 46	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
48		linecom 30702	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ Line Line
49	38, 39, 42, 44, 48	syl13anc 1266	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
50	47, 49	eqtrd 2470	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
51	36	simplld 759	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
52	51, 50	eleqtrd 2519	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
53		simp2rl 1074	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
54		simp2lr 1073	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
55	54	necomd 2702	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
56		lineelsb2 30700	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
57	38, 42, 39, 43, 53, 55, 56	syl132anc 1282	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line Line
58	52, 57	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
59		linecom 30702	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ Line Line
60	38, 42, 53, 55, 59	syl13anc 1266	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
61	50, 58, 60	3eqtrd 2474	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
62	61	3expa 1205	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
63	62	expcom 436	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
64	34, 63	pm2.61ine 2744	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
65	64	expr 618	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ Line Line
66	9, 11, 65	mp2and 683	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line Line
67	66	ex 435	. . . . . . . 8 $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line Line
68		eleq2 2502	. . . . . . . . . . 11 Line Line
69		eleq2 2502	. . . . . . . . . . 11 Line Line
70	68, 69	anbi12d 715	. . . . . . . . . 10 Line $/\$ Line $/\$ Line
71	70	anbi1d 709	. . . . . . . . 9 Line $/\$ $/\$ Line $/\$ Line $/\$
72		eqeq1 2433	. . . . . . . . 9 Line Line Line Line
73	71, 72	imbi12d 321	. . . . . . . 8 Line $/\$ $/\$ Line Line $/\$ Line $/\$ Line Line
74	67, 73	syl5ibrcom 225	. . . . . . 7 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
75	74	expimpd 606	. . . . . 6 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
76	75	3expa 1205	. . . . 5 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
77	76	rexlimdva 2924	. . . 4 $/\$ $/\$ Line $/\$ $/\$ Line
78	77	rexlimivv 2929	. . 3 $/\$ Line $/\$ $/\$ Line
79	1, 78	sylbi 198	. 2 LinesEE $/\$ $/\$ Line
80	79	3impib 1203	1 LinesEE $/\$ $/\$ $/\$ Line

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1437

wcel 1870

wne 2625

wrex 2783

wss 3442

cfv 5601 (class class class)co 6305

cn 10609

cee 24764 Linecline2 30686 LinesEEclines2 30688

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-inf2 8146 ax-cnex 9594 ax-resscn 9595 ax-1cn 9596 ax-icn 9597 ax-addcl 9598 ax-addrcl 9599 ax-mulcl 9600 ax-mulrcl 9601 ax-mulcom 9602 ax-addass 9603 ax-mulass 9604 ax-distr 9605 ax-i2m1 9606 ax-1ne0 9607 ax-1rid 9608 ax-rnegex 9609 ax-rrecex 9610 ax-cnre 9611 ax-pre-lttri 9612 ax-pre-lttrn 9613 ax-pre-ltadd 9614 ax-pre-mulgt0 9615 ax-pre-sup 9616

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-pss 3458 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-tp 4007 df-op 4009 df-uni 4223 df-int 4259 df-iun 4304 df-br 4427 df-opab 4485 df-mpt 4486 df-tr 4521 df-eprel 4765 df-id 4769 df-po 4775 df-so 4776 df-fr 4813 df-se 4814 df-we 4815 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-om 6707 df-1st 6807 df-2nd 6808 df-wrecs 7036 df-recs 7098 df-rdg 7136 df-1o 7190 df-oadd 7194 df-er 7371 df-ec 7373 df-map 7482 df-en 7578 df-dom 7579 df-sdom 7580 df-fin 7581 df-sup 7962 df-oi 8025 df-card 8372 df-pnf 9676 df-mnf 9677 df-xr 9678 df-ltxr 9679 df-le 9680 df-sub 9861 df-neg 9862 df-div 10269 df-nn 10610 df-2 10668 df-3 10669 df-n0 10870 df-z 10938 df-uz 11160 df-rp 11303 df-ico 11641 df-icc 11642 df-fz 11783 df-fzo 11914 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13141 df-re 13142 df-im 13143 df-sqrt 13277 df-abs 13278 df-clim 13530 df-sum 13731 df-ee 24767 df-btwn 24768 df-cgr 24769 df-ofs 30535 df-colinear 30591 df-ifs 30592 df-cgr3 30593 df-fs 30594 df-line2 30689 df-lines2 30691

This theorem is referenced by: hilbert1.2 30707 lineintmo 30709

W3C validator