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 
|- P = ( Base ` G )
tglngval.l 
|- L = ( LineG ` G )
tglngval.i 
|- I = ( Itv ` G )
tglngval.g 
|- ( ph -> G e. TarskiG )
tglngval.x 
|- ( ph -> X e. P )
tglngval.y 
|- ( ph -> Y e. P )
tgcolg.z 
|- ( ph -> Z e. P )
lnxfr.r 
|- .~ = ( cgrG ` G )
lnxfr.a 
|- ( ph -> A e. P )
lnxfr.b 
|- ( ph -> B e. P )
lnxfr.d 
|- .- = ( dist ` G )
tgidinside.1 
|- ( ph -> Z e. ( X I Y ) )
tgidinside.2 
|- ( ph -> ( X .- Z ) = ( X .- A ) )
tgidinside.3 
|- ( ph -> ( Y .- Z ) = ( Y .- A ) )
Assertion tgidinside 
|- ( ph -> Z = A )

Proof

Step Hyp Ref Expression
1 tglngval.p 
 |-  P = ( Base ` G )
2 tglngval.l 
 |-  L = ( LineG ` G )
3 tglngval.i 
 |-  I = ( Itv ` G )
4 tglngval.g 
 |-  ( ph -> G e. TarskiG )
5 tglngval.x 
 |-  ( ph -> X e. P )
6 tglngval.y 
 |-  ( ph -> Y e. P )
7 tgcolg.z 
 |-  ( ph -> Z e. P )
8 lnxfr.r 
 |-  .~ = ( cgrG ` G )
9 lnxfr.a 
 |-  ( ph -> A e. P )
10 lnxfr.b 
 |-  ( ph -> B e. P )
11 lnxfr.d 
 |-  .- = ( dist ` G )
12 tgidinside.1 
 |-  ( ph -> Z e. ( X I Y ) )
13 tgidinside.2 
 |-  ( ph -> ( X .- Z ) = ( X .- A ) )
14 tgidinside.3 
 |-  ( ph -> ( Y .- Z ) = ( Y .- A ) )
15 4 adantr 
 |-  ( ( ph /\ X = Y ) -> G e. TarskiG )
16 5 adantr 
 |-  ( ( ph /\ X = Y ) -> X e. P )
17 7 adantr 
 |-  ( ( ph /\ X = Y ) -> Z e. P )
18 12 adantr 
 |-  ( ( ph /\ X = Y ) -> Z e. ( X I Y ) )
19 simpr 
 |-  ( ( ph /\ X = Y ) -> X = Y )
20 19 oveq2d 
 |-  ( ( ph /\ X = Y ) -> ( X I X ) = ( X I Y ) )
21 18 20 eleqtrrd 
 |-  ( ( ph /\ X = Y ) -> Z e. ( X I X ) )
22 1 11 3 15 16 17 21 axtgbtwnid 
 |-  ( ( ph /\ X = Y ) -> X = Z )
23 9 adantr 
 |-  ( ( ph /\ X = Y ) -> A e. P )
24 13 adantr 
 |-  ( ( ph /\ X = Y ) -> ( X .- Z ) = ( X .- A ) )
25 1 11 3 15 16 17 16 23 24 22 tgcgreq 
 |-  ( ( ph /\ X = Y ) -> X = A )
26 22 25 eqtr3d 
 |-  ( ( ph /\ X = Y ) -> Z = A )
27 4 adantr 
 |-  ( ( ph /\ X =/= Y ) -> G e. TarskiG )
28 5 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. P )
29 6 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. P )
30 7 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Z e. P )
31 9 adantr 
 |-  ( ( ph /\ X =/= Y ) -> A e. P )
32 10 adantr 
 |-  ( ( ph /\ X =/= Y ) -> B e. P )
33 simpr 
 |-  ( ( ph /\ X =/= Y ) -> X =/= Y )
34 1 2 3 4 5 7 6 12 btwncolg3 
 |-  ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
35 34 adantr 
 |-  ( ( ph /\ X =/= Y ) -> ( Y e. ( X L Z ) \/ X = Z ) )
36 13 adantr 
 |-  ( ( ph /\ X =/= Y ) -> ( X .- Z ) = ( X .- A ) )
37 14 adantr 
 |-  ( ( ph /\ X =/= Y ) -> ( Y .- Z ) = ( Y .- A ) )
38 1 2 3 27 28 29 30 8 31 32 11 33 35 36 37 lnid 
 |-  ( ( ph /\ X =/= Y ) -> Z = A )
39 26 38 pm2.61dane 
 |-  ( ph -> Z = A )