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 29380

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 29379	. . 3 LinesEE $/\$ Line
2		simpll1 1035	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
3		simpll2 1036	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
4		simpll3 1037	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
5		simplr 754	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
6		liness 29372	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ Line
7	2, 3, 4, 5, 6	syl13anc 1230	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
8		simprll 761	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
9	7, 8	sseldd 3505	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
10		simprlr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
11	7, 10	sseldd 3505	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
12		simplll 757	. . . . . . . . . . . . . . . 16 Line $/\$ Line $/\$ $/\$ $/\$ Line
13	12	adantl 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line
14		simpll1 1035	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
15		simpll2 1036	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
16		simpll3 1037	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
17		simplr 754	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
18		simprrl 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
19		simprlr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
20	19	necomd 2738	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
21		lineelsb2 29375	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
22	14, 15, 16, 17, 18, 20, 21	syl132anc 1246	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line Line
23	13, 22	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
24		linecom 29377	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ Line Line
25	14, 15, 18, 20, 24	syl13anc 1230	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
26	23, 25	eqtrd 2508	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
27		neeq2 2750	. . . . . . . . . . . . . . . . 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 6290	. . . . . . . . . . . . . . 15 Line Line
32	31	eqeq2d 2481	. . . . . . . . . . . . . 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 996	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simp2l 1022	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
37	35, 36, 10	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
38		simp1l1 1089	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
39		simp1l2 1090	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
40		simp1l3 1091	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
41		simp1r 1021	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
42		simp2rr 1066	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
43		simp3 998	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
44	43	necomd 2738	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
45		lineelsb2 29375	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
46	38, 39, 40, 41, 42, 44, 45	syl132anc 1246	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line Line
47	37, 46	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
48		linecom 29377	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ Line Line
49	38, 39, 42, 44, 48	syl13anc 1230	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
50	47, 49	eqtrd 2508	. . . . . . . . . . . . . . 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 2557	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
54		simp2rl 1065	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
55		simp2lr 1064	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
56	55	necomd 2738	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
57		lineelsb2 29375	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
58	38, 42, 39, 43, 54, 56, 57	syl132anc 1246	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line Line
59	53, 58	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
60		linecom 29377	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ Line Line
61	38, 42, 54, 56, 60	syl13anc 1230	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
62	50, 59, 61	3eqtrd 2512	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
63	62	3expa 1196	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
64	63	expcom 435	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
65	34, 64	pm2.61ine 2780	. . . . . . . . . . 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 2540	. . . . . . . . . . 11 Line Line
70		eleq2 2540	. . . . . . . . . . 11 Line Line
71	69, 70	anbi12d 710	. . . . . . . . . 10 Line $/\$ Line $/\$ Line
72	71	anbi1d 704	. . . . . . . . 9 Line $/\$ $/\$ Line $/\$ Line $/\$
73		eqeq1 2471	. . . . . . . . 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 1196	. . . . 5 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
78	77	rexlimdva 2955	. . . 4 $/\$ $/\$ Line $/\$ $/\$ Line
79	78	rexlimivv 2960	. . 3 $/\$ Line $/\$ $/\$ Line
80	1, 79	sylbi 195	. 2 LinesEE $/\$ $/\$ Line
81	80	3impib 1194	1 LinesEE $/\$ $/\$ $/\$ Line

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1379

wcel 1767

wne 2662

wrex 2815

wss 3476

cfv 5586 (class class class)co 6282

cn 10532

cee 23867 Linecline2 29361 LinesEEclines2 29363

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-oadd 7131 df-er 7308 df-ec 7310 df-map 7419 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-sup 7897 df-oi 7931 df-card 8316 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-n0 10792 df-z 10861 df-uz 11079 df-rp 11217 df-ico 11531 df-icc 11532 df-fz 11669 df-fzo 11789 df-seq 12072 df-exp 12131 df-hash 12370 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-clim 13270 df-sum 13468 df-ee 23870 df-btwn 23871 df-cgr 23872 df-ofs 29210 df-colinear 29266 df-ifs 29267 df-cgr3 29268 df-fs 29269 df-line2 29364 df-lines2 29366

This theorem is referenced by: hilbert1.2 29382 lineintmo 29384

W3C validator