Metamath Proof Explorer

Theorem tglineelsb2

Description: If S lies on PQ , then PQ = PS . Theorem 6.16 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 17-May-2019)

Ref Expression
Hypotheses tglineelsb2.p ⊢ 𝐵 = ( Base ‘ 𝐺 )
tglineelsb2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglineelsb2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglineelsb2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglineelsb2.1 ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
tglineelsb2.2 ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
tglineelsb2.4 ⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
tglineelsb2.3 ⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
tglineelsb2.5 ⊢ ( 𝜑 → 𝑆 ≠ 𝑃 )
tglineelsb2.6 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑃 𝐿 𝑄 ) )
Assertion tglineelsb2 ( 𝜑 → ( 𝑃 𝐿 𝑄 ) = ( 𝑃 𝐿 𝑆 ) )

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 tglineelsb2.3 ⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
9 tglineelsb2.5 ⊢ ( 𝜑 → 𝑆 ≠ 𝑃 )
10 tglineelsb2.6 ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑃 𝐿 𝑄 ) )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝐺 ∈ TarskiG )
12 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑃 ∈ 𝐵 )
13 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑆 ∈ 𝐵 )
14 9 necomd ⊢ ( 𝜑 → 𝑃 ≠ 𝑆 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑃 ≠ 𝑆 )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑄 ∈ 𝐵 )
17 7 necomd ⊢ ( 𝜑 → 𝑄 ≠ 𝑃 )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑄 ≠ 𝑃 )
19 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑆 ∈ ( 𝑃 𝐿 𝑄 ) )
20 1 2 3 11 16 12 13 18 19 lncom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑆 ∈ ( 𝑄 𝐿 𝑃 ) )
21 1 2 3 11 12 13 16 15 20 18 lnrot1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑄 ∈ ( 𝑃 𝐿 𝑆 ) )
22 1 3 2 4 5 6 7 tglnssp ⊢ ( 𝜑 → ( 𝑃 𝐿 𝑄 ) ⊆ 𝐵 )
23 22 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑥 ∈ 𝐵 )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) )
25 1 2 3 11 12 13 15 16 18 21 23 24 tglineeltr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ) → 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) )
26 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝐺 ∈ TarskiG )
27 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝑃 ∈ 𝐵 )
28 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝑄 ∈ 𝐵 )
29 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝑃 ≠ 𝑄 )
30 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝑆 ∈ 𝐵 )
31 9 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝑆 ≠ 𝑃 )
32 10 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝑆 ∈ ( 𝑃 𝐿 𝑄 ) )
33 1 3 2 4 5 8 14 tglnssp ⊢ ( 𝜑 → ( 𝑃 𝐿 𝑆 ) ⊆ 𝐵 )
34 33 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝑥 ∈ 𝐵 )
35 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) )
36 1 2 3 26 27 28 29 30 31 32 34 35 tglineeltr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) → 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) )
37 25 36 impbida ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑃 𝐿 𝑄 ) ↔ 𝑥 ∈ ( 𝑃 𝐿 𝑆 ) ) )
38 37 eqrdv ⊢ ( 𝜑 → ( 𝑃 𝐿 𝑄 ) = ( 𝑃 𝐿 𝑆 ) )