Metamath Proof Explorer

Theorem axtgcgrrflx

Description: Axiom of reflexivity of congruence, Axiom A1 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 )
axtgcgrrflx.1 
|- ( ph -> X e. P )
axtgcgrrflx.2 
|- ( ph -> Y e. P )
Assertion axtgcgrrflx 
|- ( ph -> ( X .- Y ) = ( Y .- X ) )

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 axtgcgrrflx.1 
 |-  ( ph -> X e. P )
6 axtgcgrrflx.2 
 |-  ( ph -> Y e. P )
7 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 ) ) } ) } ) )
8 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 )
9 inss1 
 |-  ( TarskiGC i^i TarskiGB ) C_ TarskiGC
10 8 9 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
11 7 10 eqsstri 
 |-  TarskiG C_ TarskiGC
12 11 4 sseldi 
 |-  ( ph -> G e. TarskiGC )
13 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 ) ) ) )
14 13 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 ) ) )
15 14 simpld 
 |-  ( G e. TarskiGC -> A. x e. P A. y e. P ( x .- y ) = ( y .- x ) )
16 12 15 syl 
 |-  ( ph -> A. x e. P A. y e. P ( x .- y ) = ( y .- x ) )
17 oveq1 
 |-  ( x = X -> ( x .- y ) = ( X .- y ) )
18 oveq2 
 |-  ( x = X -> ( y .- x ) = ( y .- X ) )
19 17 18 eqeq12d 
 |-  ( x = X -> ( ( x .- y ) = ( y .- x ) <-> ( X .- y ) = ( y .- X ) ) )
20 oveq2 
 |-  ( y = Y -> ( X .- y ) = ( X .- Y ) )
21 oveq1 
 |-  ( y = Y -> ( y .- X ) = ( Y .- X ) )
22 20 21 eqeq12d 
 |-  ( y = Y -> ( ( X .- y ) = ( y .- X ) <-> ( X .- Y ) = ( Y .- X ) ) )
23 19 22 rspc2v 
 |-  ( ( X e. P /\ Y e. P ) -> ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) -> ( X .- Y ) = ( Y .- X ) ) )
24 5 6 23 syl2anc 
 |-  ( ph -> ( A. x e. P A. y e. P ( x .- y ) = ( y .- x ) -> ( X .- Y ) = ( Y .- X ) ) )
25 16 24 mpd 
 |-  ( ph -> ( X .- Y ) = ( Y .- X ) )