linethru - Mathbox for Scott Fenton

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

Theorem linethru 25991

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 25990	. . 3 LinesEE $/\$ Line
2		simpll1 996	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
3		simpll2 997	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
4		simpll3 998	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
5		simplr 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
6		liness 25983	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ Line
7	2, 3, 4, 5, 6	syl13anc 1186	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
8		simprll 739	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
9	7, 8	sseldd 3309	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
10		simprlr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line
11	7, 10	sseldd 3309	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
12		simplll 735	. . . . . . . . . . . . . . . 16 Line $/\$ Line $/\$ $/\$ $/\$ Line
13	12	adantl 453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line
14		simpll1 996	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
15		simpll2 997	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
16		simpll3 998	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
17		simplr 732	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
18		simprrl 741	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
19		simprlr 740	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
20	19	necomd 2650	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
21		lineelsb2 25986	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
22	14, 15, 16, 17, 18, 20, 21	syl132anc 1202	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line Line
23	13, 22	mpd 15	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
24		linecom 25988	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ Line Line
25	14, 15, 18, 20, 24	syl13anc 1186	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
26	23, 25	eqtrd 2436	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
27		neeq2 2576	. . . . . . . . . . . . . . . . 17
28	27	anbi2d 685	. . . . . . . . . . . . . . . 16 Line $/\$ Line $/\$ Line $/\$ Line $/\$
29	28	anbi1d 686	. . . . . . . . . . . . . . 15 Line $/\$ Line $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
30	29	anbi2d 685	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$
31		oveq2 6048	. . . . . . . . . . . . . . 15 Line Line
32	31	eqeq2d 2415	. . . . . . . . . . . . . 14 Line Line Line Line
33	30, 32	imbi12d 312	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
34	26, 33	mpbiri 225	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
35		simp1 957	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simp2l 983	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$
37	35, 36, 10	syl2anc 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
38		simp1l1 1050	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
39		simp1l2 1051	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
40		simp1l3 1052	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
41		simp1r 982	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
42		simp2rr 1027	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
43		simp3 959	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
44	43	necomd 2650	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
45		lineelsb2 25986	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
46	38, 39, 40, 41, 42, 44, 45	syl132anc 1202	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line Line
47	37, 46	mpd 15	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
48		linecom 25988	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ Line Line
49	38, 39, 42, 44, 48	syl13anc 1186	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
50	47, 49	eqtrd 2436	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
51		simpll 731	. . . . . . . . . . . . . . . . . 18 Line $/\$ Line $/\$ Line
52	36, 51	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
53	52, 50	eleqtrd 2480	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line
54		simp2rl 1026	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
55		simp2lr 1025	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
56	55	necomd 2650	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$
57		lineelsb2 25986	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ Line Line Line
58	38, 42, 39, 43, 54, 56, 57	syl132anc 1202	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line Line
59	53, 58	mpd 15	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
60		linecom 25988	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ Line Line
61	38, 42, 54, 56, 60	syl13anc 1186	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
62	50, 59, 61	3eqtrd 2440	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
63	62	3expa 1153	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ $/\$ Line Line
64	63	expcom 425	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
65	34, 64	pm2.61ine 2643	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ $/\$ Line Line
66	65	expr 599	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ $/\$ Line Line
67	9, 11, 66	mp2and 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line Line
68	67	ex 424	. . . . . . . 8 $/\$ $/\$ $/\$ Line $/\$ Line $/\$ Line Line
69		eleq2 2465	. . . . . . . . . . 11 Line Line
70		eleq2 2465	. . . . . . . . . . 11 Line Line
71	69, 70	anbi12d 692	. . . . . . . . . 10 Line $/\$ Line $/\$ Line
72	71	anbi1d 686	. . . . . . . . 9 Line $/\$ $/\$ Line $/\$ Line $/\$
73		eqeq1 2410	. . . . . . . . 9 Line Line Line Line
74	72, 73	imbi12d 312	. . . . . . . 8 Line $/\$ $/\$ Line Line $/\$ Line $/\$ Line Line
75	68, 74	syl5ibrcom 214	. . . . . . 7 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
76	75	expimpd 587	. . . . . 6 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
77	76	3expa 1153	. . . . 5 $/\$ $/\$ $/\$ Line $/\$ $/\$ Line
78	77	rexlimdva 2790	. . . 4 $/\$ $/\$ Line $/\$ $/\$ Line
79	78	rexlimivv 2795	. . 3 $/\$ Line $/\$ $/\$ Line
80	1, 79	sylbi 188	. 2 LinesEE $/\$ $/\$ Line
81	80	3impib 1151	1 LinesEE $/\$ $/\$ $/\$ Line

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wne 2567

wrex 2667

wss 3280

cfv 5413 (class class class)co 6040

cn 9956

cee 25731 Linecline2 25972 LinesEEclines2 25974

This theorem is referenced by: hilbert1.2 25993 lineintmo 25995

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-ec 6866 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-n0 10178 df-z 10239 df-uz 10445 df-rp 10569 df-ico 10878 df-icc 10879 df-fz 11000 df-fzo 11091 df-seq 11279 df-exp 11338 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-sum 12435 df-ee 25734 df-btwn 25735 df-cgr 25736 df-ofs 25821 df-ifs 25877 df-cgr3 25878 df-colinear 25879 df-fs 25880 df-line2 25975 df-lines2 25977

W3C validator