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 ( 𝜑𝑍 = 𝐴 )