Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
tglineelsb2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglineelsb2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglineelsb2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglineelsb2.1 ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
tglineelsb2.2 ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
tglineelsb2.4 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
tglinethru.0 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
tglinethru.1 ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
tglinethru.2 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
tglinethru.3 ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion tglinethru ( 𝜑 → 𝐴 = ( 𝑃 𝐿 𝑄 ) )

Proof

Step Hyp Ref Expression
1 tglineelsb2.p ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tglineelsb2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tglineelsb2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tglineelsb2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tglineelsb2.1 ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6 tglineelsb2.2 ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
7 tglineelsb2.4 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
8 tglinethru.0 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
9 tglinethru.1 ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
10 tglinethru.2 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
11 tglinethru.3 ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
12 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝐺 ∈ TarskiG )
13 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑥 ∈ 𝐵 )
14 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑦 ∈ 𝐵 )
15 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑥 ≠ 𝑦 )
16 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑄 ∈ 𝐵 )
17 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑃 ≠ 𝑄 )
18 17 necomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑄 ≠ 𝑃 )
19 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑃 = 𝑥 )
20 18 19 neeqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑄 ≠ 𝑥 )
21 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑄 ∈ 𝐴 )
22 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
23 21 22 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝑄 ∈ ( 𝑥 𝐿 𝑦 ) )
24 1 2 3 12 13 14 15 16 20 23 tglineelsb2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → ( 𝑥 𝐿 𝑦 ) = ( 𝑥 𝐿 𝑄 ) )
25 19 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → ( 𝑃 𝐿 𝑄 ) = ( 𝑥 𝐿 𝑄 ) )
26 24 22 25 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 = 𝑥 ) → 𝐴 = ( 𝑃 𝐿 𝑄 ) )
27 simplrl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
28 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝐺 ∈ TarskiG )
29 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑥 ∈ 𝐵 )
30 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑦 ∈ 𝐵 )
31 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑥 ≠ 𝑦 )
32 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑃 ∈ 𝐵 )
33 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑃 ≠ 𝑥 )
34 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑃 ∈ 𝐴 )
35 34 27 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑃 ∈ ( 𝑥 𝐿 𝑦 ) )
36 1 2 3 28 29 30 31 32 33 35 tglineelsb2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → ( 𝑥 𝐿 𝑦 ) = ( 𝑥 𝐿 𝑃 ) )
37 33 necomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑥 ≠ 𝑃 )
38 1 2 3 28 29 32 37 tglinecom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → ( 𝑥 𝐿 𝑃 ) = ( 𝑃 𝐿 𝑥 ) )
39 27 36 38 3eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝐴 = ( 𝑃 𝐿 𝑥 ) )
40 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑄 ∈ 𝐵 )
41 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑃 ≠ 𝑄 )
42 41 necomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑄 ≠ 𝑃 )
43 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑄 ∈ 𝐴 )
44 43 39 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝑄 ∈ ( 𝑃 𝐿 𝑥 ) )
45 1 2 3 28 32 29 33 40 42 44 tglineelsb2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → ( 𝑃 𝐿 𝑥 ) = ( 𝑃 𝐿 𝑄 ) )
46 39 45 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑃 ≠ 𝑥 ) → 𝐴 = ( 𝑃 𝐿 𝑄 ) )
47 26 46 pm2.61dane ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐴 = ( 𝑃 𝐿 𝑄 ) )
48 1 2 3 4 9 tgisline ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
49 47 48 r19.29vva ⊢ ( 𝜑 → 𝐴 = ( 𝑃 𝐿 𝑄 ) )