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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
axtrkg.d ⊢ − = ( dist ‘ 𝐺 )
axtrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
axtrkg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
axtgcgrrflx.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
axtgcgrrflx.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
Assertion axtgcgrrflx ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑌 − 𝑋 ) )

Proof

Step Hyp Ref Expression
1 axtrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 axtrkg.d ⊢ − = ( dist ‘ 𝐺 )
3 axtrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 axtrkg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 axtgcgrrflx.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 axtgcgrrflx.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 df-trkg ⊢ TarskiG = ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) )
8 inss1 ⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ ( TarskiGC ∩ TarskiGB )
9 inss1 ⊢ ( TarskiGC ∩ TarskiGB ) ⊆ TarskiGC
10 8 9 sstri ⊢ ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥 ∈ 𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧 ∈ 𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ TarskiGC
11 7 10 eqsstri ⊢ TarskiG ⊆ TarskiGC
12 11 4 sseldi ⊢ ( 𝜑 → 𝐺 ∈ TarskiGC )
13 1 2 3 istrkgc ⊢ ( 𝐺 ∈ TarskiGC ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) ) )
14 13 simprbi ⊢ ( 𝐺 ∈ TarskiGC → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) )
15 14 simpld ⊢ ( 𝐺 ∈ TarskiGC → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) )
16 12 15 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) )
17 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 𝑦 ) = ( 𝑋 − 𝑦 ) )
18 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑦 − 𝑥 ) = ( 𝑦 − 𝑋 ) )
19 17 18 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ↔ ( 𝑋 − 𝑦 ) = ( 𝑦 − 𝑋 ) ) )
20 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 − 𝑦 ) = ( 𝑋 − 𝑌 ) )
21 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 − 𝑋 ) = ( 𝑌 − 𝑋 ) )
22 20 21 eqeq12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 − 𝑦 ) = ( 𝑦 − 𝑋 ) ↔ ( 𝑋 − 𝑌 ) = ( 𝑌 − 𝑋 ) ) )
23 19 22 rspc2v ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) → ( 𝑋 − 𝑌 ) = ( 𝑌 − 𝑋 ) ) )
24 5 6 23 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) → ( 𝑋 − 𝑌 ) = ( 𝑌 − 𝑋 ) ) )
25 16 24 mpd ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑌 − 𝑋 ) )