Metamath Proof Explorer


Theorem lncgr

Description: Congruence rule for lines. Theorem 4.17 of Schwabhauser p. 37. (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 )
lncgr.1
|- ( ph -> X =/= Y )
lncgr.2
|- ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
lncgr.3
|- ( ph -> ( X .- A ) = ( X .- B ) )
lncgr.4
|- ( ph -> ( Y .- A ) = ( Y .- B ) )
Assertion lncgr
|- ( ph -> ( Z .- A ) = ( Z .- B ) )

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 lncgr.1
 |-  ( ph -> X =/= Y )
13 lncgr.2
 |-  ( ph -> ( Y e. ( X L Z ) \/ X = Z ) )
14 lncgr.3
 |-  ( ph -> ( X .- A ) = ( X .- B ) )
15 lncgr.4
 |-  ( ph -> ( Y .- A ) = ( Y .- B ) )
16 1 11 3 8 4 5 6 7 cgr3id
 |-  ( ph -> <" X Y Z "> .~ <" X Y Z "> )
17 1 2 3 4 5 6 7 8 5 6 11 9 7 10 13 16 14 15 12 tgfscgr
 |-  ( ph -> ( Z .- A ) = ( Z .- B ) )