Metamath Proof Explorer

Theorem tgidinside

Description: Law for finding a point inside a segment. Theorem 4.19 of Schwabhauser p. 38. (Contributed by Thierry Arnoux, 28-Apr-2019)

Ref Expression
Hypotheses tglngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglngval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglngval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
tglngval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
tgcolg.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
lnxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
lnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
lnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
lnxfr.d ⊢ − = ( dist ‘ 𝐺 )
tgidinside.1 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) )
tgidinside.2 ⊢ ( 𝜑 → ( 𝑋 − 𝑍 ) = ( 𝑋 − 𝐴 ) )
tgidinside.3 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑌 − 𝐴 ) )
Assertion tgidinside ( 𝜑 → 𝑍 = 𝐴 )

Proof

Step Hyp Ref Expression
1 tglngval.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglngval.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 tglngval.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tglngval.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tglngval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 tglngval.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 tgcolg.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 lnxfr.r ⊢ ∼ = ( cgrG ‘ 𝐺 )
9 lnxfr.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
10 lnxfr.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
11 lnxfr.d ⊢ − = ( dist ‘ 𝐺 )
12 tgidinside.1 ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) )
13 tgidinside.2 ⊢ ( 𝜑 → ( 𝑋 − 𝑍 ) = ( 𝑋 − 𝐴 ) )
14 tgidinside.3 ⊢ ( 𝜑 → ( 𝑌 − 𝑍 ) = ( 𝑌 − 𝐴 ) )
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝐺 ∈ TarskiG )
16 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 ∈ 𝑃 )
17 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑍 ∈ 𝑃 )
18 12 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) )
19 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
20 19 oveq2d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑋 𝐼 𝑋 ) = ( 𝑋 𝐼 𝑌 ) )
21 18 20 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑍 ∈ ( 𝑋 𝐼 𝑋 ) )
22 1 11 3 15 16 17 21 axtgbtwnid ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑍 )
23 9 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝐴 ∈ 𝑃 )
24 13 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑋 − 𝑍 ) = ( 𝑋 − 𝐴 ) )
25 1 11 3 15 16 17 16 23 24 22 tgcgreq ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝐴 )
26 22 25 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑍 = 𝐴 )
27 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐺 ∈ TarskiG )
28 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝑃 )
29 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝑃 )
30 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑍 ∈ 𝑃 )
31 9 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐴 ∈ 𝑃 )
32 10 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐵 ∈ 𝑃 )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
34 1 2 3 4 5 7 6 12 btwncolg3 ⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∨ 𝑋 = 𝑍 ) )
36 13 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑋 − 𝑍 ) = ( 𝑋 − 𝐴 ) )
37 14 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 − 𝑍 ) = ( 𝑌 − 𝐴 ) )
38 1 2 3 27 28 29 30 8 31 32 11 33 35 36 37 lnid ⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑍 = 𝐴 )
39 26 38 pm2.61dane ⊢ ( 𝜑 → 𝑍 = 𝐴 )