Metamath Proof Explorer

Theorem axtgcgrid

Description: Axiom of identity of congruence, Axiom A3 of Schwabhauser p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019)

Ref Expression
Hypotheses axtrkg.p 
|- P = ( Base ` G )
axtrkg.d 
|- .- = ( dist ` G )
axtrkg.i 
|- I = ( Itv ` G )
axtrkg.g 
|- ( ph -> G e. TarskiG )
axtgcgrid.1 
|- ( ph -> X e. P )
axtgcgrid.2 
|- ( ph -> Y e. P )
axtgcgrid.3 
|- ( ph -> Z e. P )
axtgcgrid.4 
|- ( ph -> ( X .- Y ) = ( Z .- Z ) )
Assertion axtgcgrid 
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 axtrkg.p 
 |-  P = ( Base ` G )
2 axtrkg.d 
 |-  .- = ( dist ` G )
3 axtrkg.i 
 |-  I = ( Itv ` G )
4 axtrkg.g 
 |-  ( ph -> G e. TarskiG )
5 axtgcgrid.1 
 |-  ( ph -> X e. P )
6 axtgcgrid.2 
 |-  ( ph -> Y e. P )
7 axtgcgrid.3 
 |-  ( ph -> Z e. P )
8 axtgcgrid.4 
 |-  ( ph -> ( X .- Y ) = ( Z .- Z ) )
9 df-trkg 
 |-  TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
10 inss1 
 |-  ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ ( TarskiGC i^i TarskiGB )
11 inss1 
 |-  ( TarskiGC i^i TarskiGB ) C_ TarskiGC
12 10 11 sstri 
 |-  ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ TarskiGC
13 9 12 eqsstri 
 |-  TarskiG C_ TarskiGC
14 13 4 sseldi 
 |-  ( ph -> G e. TarskiGC )
15 1 2 3 istrkgc 
 |-  ( G e. TarskiGC <-> ( G e. _V /\ ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) ) )
16 15 simprbi 
 |-  ( G e. TarskiGC -> ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) /\ A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) ) )
17 16 simprd 
 |-  ( G e. TarskiGC -> A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) )
18 14 17 syl 
 |-  ( ph -> A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) )
19 oveq1 
 |-  ( x = X -> ( x .- y ) = ( X .- y ) )
20 19 eqeq1d 
 |-  ( x = X -> ( ( x .- y ) = ( z .- z ) <-> ( X .- y ) = ( z .- z ) ) )
21 eqeq1 
 |-  ( x = X -> ( x = y <-> X = y ) )
22 20 21 imbi12d 
 |-  ( x = X -> ( ( ( x .- y ) = ( z .- z ) -> x = y ) <-> ( ( X .- y ) = ( z .- z ) -> X = y ) ) )
23 oveq2 
 |-  ( y = Y -> ( X .- y ) = ( X .- Y ) )
24 23 eqeq1d 
 |-  ( y = Y -> ( ( X .- y ) = ( z .- z ) <-> ( X .- Y ) = ( z .- z ) ) )
25 eqeq2 
 |-  ( y = Y -> ( X = y <-> X = Y ) )
26 24 25 imbi12d 
 |-  ( y = Y -> ( ( ( X .- y ) = ( z .- z ) -> X = y ) <-> ( ( X .- Y ) = ( z .- z ) -> X = Y ) ) )
27 id 
 |-  ( z = Z -> z = Z )
28 27 27 oveq12d 
 |-  ( z = Z -> ( z .- z ) = ( Z .- Z ) )
29 28 eqeq2d 
 |-  ( z = Z -> ( ( X .- Y ) = ( z .- z ) <-> ( X .- Y ) = ( Z .- Z ) ) )
30 29 imbi1d 
 |-  ( z = Z -> ( ( ( X .- Y ) = ( z .- z ) -> X = Y ) <-> ( ( X .- Y ) = ( Z .- Z ) -> X = Y ) ) )
31 22 26 30 rspc3v 
 |-  ( ( X e. P /\ Y e. P /\ Z e. P ) -> ( A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) -> ( ( X .- Y ) = ( Z .- Z ) -> X = Y ) ) )
32 5 6 7 31 syl3anc 
 |-  ( ph -> ( A. x e. P A. y e. P A. z e. P ( ( x .- y ) = ( z .- z ) -> x = y ) -> ( ( X .- Y ) = ( Z .- Z ) -> X = Y ) ) )
33 18 8 32 mp2d 
 |-  ( ph -> X = Y )