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 28189

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 28188	. . 3 LinesEE $/\$ Line
2		simpll1 1027	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
3		simpll2 1028	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
4		simpll3 1029	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
5		simplr 754	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
6		liness 28181	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ Line
7	2, 3, 4, 5, 6	syl13anc 1220	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
8		simprll 761	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
9	7, 8	sseldd 3362	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
10		simprlr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
11	7, 10	sseldd 3362	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
12		simplll 757	. . . . . . . . . . . . . . . 16 Line $/\$ Line $/\$ $/\$ $/\$ Line
13	12	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line
14		simpll1 1027	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
15		simpll2 1028	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
16		simpll3 1029	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
17		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
18		simprrl 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
19		simprlr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
20	19	necomd 2700	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
21		lineelsb2 28184	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
22	14, 15, 16, 17, 18, 20, 21	syl132anc 1236	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line Line
23	13, 22	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
24		linecom 28186	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ Line Line
25	14, 15, 18, 20, 24	syl13anc 1220	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
26	23, 25	eqtrd 2475	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
27		neeq2 2622	. . . . . . . . . . . . . . . . 17
28	27	anbi2d 703	. . . . . . . . . . . . . . . 16 Line $/\$ Line $/\$ Line $/\$ Line $/\$
29	28	anbi1d 704	. . . . . . . . . . . . . . 15 Line $/\$ Line $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
30	29	anbi2d 703	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
31		oveq2 6104	. . . . . . . . . . . . . . 15 Line Line
32	31	eqeq2d 2454	. . . . . . . . . . . . . 14 Line Line Line Line
33	30, 32	imbi12d 320	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
34	26, 33	mpbiri 233	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
35		simp1 988	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simp2l 1014	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
37	35, 36, 10	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
38		simp1l1 1081	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
39		simp1l2 1082	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
40		simp1l3 1083	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
41		simp1r 1013	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
42		simp2rr 1058	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
43		simp3 990	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
44	43	necomd 2700	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
45		lineelsb2 28184	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
46	38, 39, 40, 41, 42, 44, 45	syl132anc 1236	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line Line
47	37, 46	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
48		linecom 28186	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ Line Line
49	38, 39, 42, 44, 48	syl13anc 1220	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
50	47, 49	eqtrd 2475	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
51		simpll 753	. . . . . . . . . . . . . . . . . 18 Line $/\$ Line $/\$ Line
52	36, 51	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
53	52, 50	eleqtrd 2519	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
54		simp2rl 1057	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
55		simp2lr 1056	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
56	55	necomd 2700	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
57		lineelsb2 28184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
58	38, 42, 39, 43, 54, 56, 57	syl132anc 1236	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line Line
59	53, 58	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
60		linecom 28186	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ Line Line
61	38, 42, 54, 56, 60	syl13anc 1220	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
62	50, 59, 61	3eqtrd 2479	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
63	62	3expa 1187	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
64	63	expcom 435	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
65	34, 64	pm2.61ine 2692	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
66	65	expr 615	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ Line Line
67	9, 11, 66	mp2and 679	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line Line
68	67	ex 434	. . . . . . . 8 $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line Line
69		eleq2 2504	. . . . . . . . . . 11 Line Line
70		eleq2 2504	. . . . . . . . . . 11 Line Line
71	69, 70	anbi12d 710	. . . . . . . . . 10 Line $/\$ Line $/\$ Line
72	71	anbi1d 704	. . . . . . . . 9 Line $/\$ $/\$ Line $/\$ Line $/\$
73		eqeq1 2449	. . . . . . . . 9 Line Line Line Line
74	72, 73	imbi12d 320	. . . . . . . 8 Line $/\$ $/\$ Line Line $/\$ Line $/\$ Line Line
75	68, 74	syl5ibrcom 222	. . . . . . 7 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
76	75	expimpd 603	. . . . . 6 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
77	76	3expa 1187	. . . . 5 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
78	77	rexlimdva 2846	. . . 4 $/\$ $/\$ Line $/\$ $/\$ Line
79	78	rexlimivv 2851	. . 3 $/\$ Line $/\$ $/\$ Line
80	1, 79	sylbi 195	. 2 LinesEE $/\$ $/\$ Line
81	80	3impib 1185	1 LinesEE $/\$ $/\$ $/\$ Line

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1369

wcel 1756

wne 2611

wrex 2721

wss 3333

cfv 5423 (class class class)co 6096

cn 10327

cee 23139 Linecline2 28170 LinesEEclines2 28172

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4408 ax-sep 4418 ax-nul 4426 ax-pow 4475 ax-pr 4536 ax-un 6377 ax-inf2 7852 ax-cnex 9343 ax-resscn 9344 ax-1cn 9345 ax-icn 9346 ax-addcl 9347 ax-addrcl 9348 ax-mulcl 9349 ax-mulrcl 9350 ax-mulcom 9351 ax-addass 9352 ax-mulass 9353 ax-distr 9354 ax-i2m1 9355 ax-1ne0 9356 ax-1rid 9357 ax-rnegex 9358 ax-rrecex 9359 ax-cnre 9360 ax-pre-lttri 9361 ax-pre-lttrn 9362 ax-pre-ltadd 9363 ax-pre-mulgt0 9364 ax-pre-sup 9365

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2573 df-ne 2613 df-nel 2614 df-ral 2725 df-rex 2726 df-reu 2727 df-rmo 2728 df-rab 2729 df-v 2979 df-sbc 3192 df-csb 3294 df-dif 3336 df-un 3338 df-in 3340 df-ss 3347 df-pss 3349 df-nul 3643 df-if 3797 df-pw 3867 df-sn 3883 df-pr 3885 df-tp 3887 df-op 3889 df-uni 4097 df-int 4134 df-iun 4178 df-br 4298 df-opab 4356 df-mpt 4357 df-tr 4391 df-eprel 4637 df-id 4641 df-po 4646 df-so 4647 df-fr 4684 df-se 4685 df-we 4686 df-ord 4727 df-on 4728 df-lim 4729 df-suc 4730 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5386 df-fun 5425 df-fn 5426 df-f 5427 df-f1 5428 df-fo 5429 df-f1o 5430 df-fv 5431 df-isom 5432 df-riota 6057 df-ov 6099 df-oprab 6100 df-mpt2 6101 df-om 6482 df-1st 6582 df-2nd 6583 df-recs 6837 df-rdg 6871 df-1o 6925 df-oadd 6929 df-er 7106 df-ec 7108 df-map 7221 df-en 7316 df-dom 7317 df-sdom 7318 df-fin 7319 df-sup 7696 df-oi 7729 df-card 8114 df-pnf 9425 df-mnf 9426 df-xr 9427 df-ltxr 9428 df-le 9429 df-sub 9602 df-neg 9603 df-div 9999 df-nn 10328 df-2 10385 df-3 10386 df-n0 10585 df-z 10652 df-uz 10867 df-rp 10997 df-ico 11311 df-icc 11312 df-fz 11443 df-fzo 11554 df-seq 11812 df-exp 11871 df-hash 12109 df-cj 12593 df-re 12594 df-im 12595 df-sqr 12729 df-abs 12730 df-clim 12971 df-sum 13169 df-ee 23142 df-btwn 23143 df-cgr 23144 df-ofs 28019 df-colinear 28075 df-ifs 28076 df-cgr3 28077 df-fs 28078 df-line2 28173 df-lines2 28175

This theorem is referenced by: hilbert1.2 28191 lineintmo 28193

W3C validator