tglinethru

Description: If A is a line containing two distinct points P and Q , then A is the line through P and Q . Theorem 6.18 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 25-May-2019)

	Ref	Expression
Hypotheses	tglineelsb2.p	$⊢ B = {Base}_{G}$
	tglineelsb2.i	$⊢ I = Itv (G)$
	tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
	tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglineelsb2.1	$⊢ φ \to P \in B$
	tglineelsb2.2	$⊢ φ \to Q \in B$
	tglineelsb2.4	$⊢ φ \to P \neq Q$
	tglinethru.0	$⊢ φ \to P \neq Q$
	tglinethru.1	$⊢ φ \to A \in ran L$
	tglinethru.2	$⊢ φ \to P \in A$
	tglinethru.3	$⊢ φ \to Q \in A$
Assertion	tglinethru	$⊢ φ \to A = P L Q$

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	$⊢ B = {Base}_{G}$
2		tglineelsb2.i	$⊢ I = Itv (G)$
3		tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglineelsb2.1	$⊢ φ \to P \in B$
6		tglineelsb2.2	$⊢ φ \to Q \in B$
7		tglineelsb2.4	$⊢ φ \to P \neq Q$
8		tglinethru.0	$⊢ φ \to P \neq Q$
9		tglinethru.1	$⊢ φ \to A \in ran L$
10		tglinethru.2	$⊢ φ \to P \in A$
11		tglinethru.3	$⊢ φ \to Q \in A$
12	4	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to G \in 𝒢_{Tarski}$
13		simp-4r	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to x \in B$
14		simpllr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to y \in B$
15		simplrr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to x \neq y$
16	6	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to Q \in B$
17	8	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to P \neq Q$
18	17	necomd	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to Q \neq P$
19		simpr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to P = x$
20	18 19	neeqtrd	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to Q \neq x$
21	11	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to Q \in A$
22		simplrl	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to A = x L y$
23	21 22	eleqtrd	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to Q \in (x L y)$
24	1 2 3 12 13 14 15 16 20 23	tglineelsb2	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to x L y = x L Q$
25	19	oveq1d	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to P L Q = x L Q$
26	24 22 25	3eqtr4d	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P = x) \to A = P L Q$
27		simplrl	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to A = x L y$
28	4	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to G \in 𝒢_{Tarski}$
29		simp-4r	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to x \in B$
30		simpllr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to y \in B$
31		simplrr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to x \neq y$
32	5	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to P \in B$
33		simpr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to P \neq x$
34	10	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to P \in A$
35	34 27	eleqtrd	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to P \in (x L y)$
36	1 2 3 28 29 30 31 32 33 35	tglineelsb2	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to x L y = x L P$
37	33	necomd	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to x \neq P$
38	1 2 3 28 29 32 37	tglinecom	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to x L P = P L x$
39	27 36 38	3eqtrd	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to A = P L x$
40	6	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to Q \in B$
41	8	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to P \neq Q$
42	41	necomd	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to Q \neq P$
43	11	ad4antr	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to Q \in A$
44	43 39	eleqtrd	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to Q \in (P L x)$
45	1 2 3 28 32 29 33 40 42 44	tglineelsb2	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to P L x = P L Q$
46	39 45	eqtrd	$⊢ ((((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \land P \neq x) \to A = P L Q$
47	26 46	pm2.61dane	$⊢ (((φ \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \to A = P L Q$
48	1 2 3 4 9	tgisline	$⊢ φ \to \exists x \in B \exists y \in B (A = x L y \land x \neq y)$
49	47 48	r19.29vva	$⊢ φ \to A = P L Q$

Metamath Proof Explorer

Theorem tglinethru

Proof