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 30926

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 30925	. . 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 30918	. . . . . . . . . . . 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 3465	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
10		simprlr 771	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
11	7, 10	sseldd 3465	. . . . . . . . . 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 2691	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
21		lineelsb2 30921	. . . . . . . . . . . . . . . 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 30923	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ Line Line
25	14, 15, 18, 20, 24	syl13anc 1266	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
26	23, 25	eqtrd 2463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
27		neeq2 2703	. . . . . . . . . . . . . . . . 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 6314	. . . . . . . . . . . . . . 15 Line Line
32	31	eqeq2d 2436	. . . . . . . . . . . . . 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 2691	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
45		lineelsb2 30921	. . . . . . . . . . . . . . . . . 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 30923	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ Line Line
49	38, 39, 42, 44, 48	syl13anc 1266	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
50	47, 49	eqtrd 2463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
51	36	simplld 759	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
52	51, 50	eleqtrd 2509	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
53		simp2rl 1074	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
54		simp2lr 1073	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
55	54	necomd 2691	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
56		lineelsb2 30921	. . . . . . . . . . . . . . . . 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 30923	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ Line Line
60	38, 42, 53, 55, 59	syl13anc 1266	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
61	50, 58, 60	3eqtrd 2467	. . . . . . . . . . . . . 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 2733	. . . . . . . . . . 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 2496	. . . . . . . . . . 11 Line Line
69		eleq2 2496	. . . . . . . . . . 11 Line Line
70	68, 69	anbi12d 715	. . . . . . . . . 10 Line $/\$ Line $/\$ Line
71	70	anbi1d 709	. . . . . . . . 9 Line $/\$ $/\$ Line $/\$ Line $/\$
72		eqeq1 2426	. . . . . . . . 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 2914	. . . 4 $/\$ $/\$ Line $/\$ $/\$ Line
78	77	rexlimivv 2919	. . 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 1872

wne 2614

wrex 2772

wss 3436

cfv 5601 (class class class)co 6306

cn 10617

cee 24917 Linecline2 30907 LinesEEclines2 30909

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6598 ax-inf2 8156 ax-cnex 9603 ax-resscn 9604 ax-1cn 9605 ax-icn 9606 ax-addcl 9607 ax-addrcl 9608 ax-mulcl 9609 ax-mulrcl 9610 ax-mulcom 9611 ax-addass 9612 ax-mulass 9613 ax-distr 9614 ax-i2m1 9615 ax-1ne0 9616 ax-1rid 9617 ax-rnegex 9618 ax-rrecex 9619 ax-cnre 9620 ax-pre-lttri 9621 ax-pre-lttrn 9622 ax-pre-ltadd 9623 ax-pre-mulgt0 9624 ax-pre-sup 9625

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 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-nel 2617 df-ral 2776 df-rex 2777 df-reu 2778 df-rmo 2779 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-int 4256 df-iun 4301 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 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 6268 df-ov 6309 df-oprab 6310 df-mpt2 6311 df-om 6708 df-1st 6808 df-2nd 6809 df-wrecs 7040 df-recs 7102 df-rdg 7140 df-1o 7194 df-oadd 7198 df-er 7375 df-ec 7377 df-map 7486 df-en 7582 df-dom 7583 df-sdom 7584 df-fin 7585 df-sup 7966 df-oi 8035 df-card 8382 df-pnf 9685 df-mnf 9686 df-xr 9687 df-ltxr 9688 df-le 9689 df-sub 9870 df-neg 9871 df-div 10278 df-nn 10618 df-2 10676 df-3 10677 df-n0 10878 df-z 10946 df-uz 11168 df-rp 11311 df-ico 11649 df-icc 11650 df-fz 11793 df-fzo 11924 df-seq 12221 df-exp 12280 df-hash 12523 df-cj 13163 df-re 13164 df-im 13165 df-sqrt 13299 df-abs 13300 df-clim 13552 df-sum 13753 df-ee 24920 df-btwn 24921 df-cgr 24922 df-ofs 30756 df-colinear 30812 df-ifs 30813 df-cgr3 30814 df-fs 30815 df-line2 30910 df-lines2 30912

This theorem is referenced by: hilbert1.2 30928 lineintmo 30930

W3C validator