Metamath Proof Explorer


Theorem lnid

Description: Identity law for points on lines. Theorem 4.18 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 )
lnid.1
|- ( ph -> X =/= Y )
lnid.2
|- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
lnid.3
|- ( ph -> ( X .- Z ) = ( X .- A ) )
lnid.4
|- ( ph -> ( Y .- Z ) = ( Y .- A ) )
Assertion lnid
|- ( 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 lnid.1
 |-  ( ph -> X =/= Y )
13 lnid.2
 |-  ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
14 lnid.3
 |-  ( ph -> ( X .- Z ) = ( X .- A ) )
15 lnid.4
 |-  ( ph -> ( Y .- Z ) = ( Y .- A ) )
16 1 2 3 4 5 6 7 8 7 9 11 12 13 14 15 lncgr
 |-  ( ph -> ( Z .- Z ) = ( Z .- A ) )
17 16 eqcomd
 |-  ( ph -> ( Z .- A ) = ( Z .- Z ) )
18 1 11 3 4 7 9 7 17 axtgcgrid
 |-  ( ph -> Z = A )