Theorem axtgcgrrflx 28389

Description: Axiom of reflexivity of congruence, Axiom A1 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.)

Hypotheses

Ref	Expression
axtrkg.p	⊢ 𝑃 = (Base‘𝐺)
axtrkg.d	⊢ − = (dist‘𝐺)
axtrkg.i	⊢ 𝐼 = (Itv‘𝐺)
axtrkg.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
axtgcgrrflx.1	⊢ (𝜑 → 𝑋 ∈ 𝑃)
axtgcgrrflx.2	⊢ (𝜑 → 𝑌 ∈ 𝑃)

Assertion

Ref	Expression
axtgcgrrflx	⊢ (𝜑 → (𝑋 − 𝑌) = (𝑌 − 𝑋))

Proof of Theorem axtgcgrrflx

Dummy variables 𝑓 𝑖 𝑝 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  {crab 3405  Vcvv 3447  [wsbc 3753   ∖ cdif 3911   ∩ cin 3913  {csn 4589  ‘cfv 6511  (class class class)co 7387   ∈ cmpo 7389  Basecbs 17179  distcds 17229  TarskiGcstrkg 28354  TarskiG_Ccstrkgc 28355  TarskiG_Bcstrkgb 28356  TarskiG_CBcstrkgcb 28357  Itvcitv 28360  LineGclng 28361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-trkgc 28375  df-trkg 28380

This theorem is referenced by:  tgcgrcomimp  28404  tgcgrcomr  28405  tgcgrcoml  28406  tgcgrcomlr  28407  tgbtwnconn1lem1  28499  tgbtwnconn1lem2  28500  tgbtwnconn1lem3  28501  miriso  28597  symquadlem  28616  midexlem  28619  footexALT  28645  footexlem1  28646  footexlem2  28647  colperpexlem1  28657  opphllem  28662  cgraswap  28747  isoas  28791  f1otrg  28798