Theorem axtgcgrid 28531

Description: Axiom of identity of congruence, Axiom A3 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)
axtgcgrid.1	⊢ (𝜑 → 𝑋 ∈ 𝑃)
axtgcgrid.2	⊢ (𝜑 → 𝑌 ∈ 𝑃)
axtgcgrid.3	⊢ (𝜑 → 𝑍 ∈ 𝑃)
axtgcgrid.4	⊢ (𝜑 → (𝑋 − 𝑌) = (𝑍 − 𝑍))

Assertion

Ref	Expression
axtgcgrid	⊢ (𝜑 → 𝑋 = 𝑌)

Proof of Theorem axtgcgrid

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

Step	Hyp	Ref	Expression
1		df-trkg 28521	. . . . 5 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss1 4177	. . . . . 6 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩ TarskiGB)
3		inss1 4177	. . . . . 6 ⊢ (TarskiGC ∩ TarskiGB) ⊆ TarskiGC
4	2, 3	sstri 3931	. . . . 5 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGC
5	1, 4	eqsstri 3968	. . . 4 ⊢ TarskiG ⊆ TarskiGC
6		axtrkg.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sselid 3919	. . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiGC)
8		axtrkg.p	. . . . . 6 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . 6 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . 6 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgc 28522	. . . . 5 ⊢ (𝐺 ∈ TarskiGC ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦))))
12	11	simprbi 497	. . . 4 ⊢ (𝐺 ∈ TarskiGC → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦)))
13	12	simprd 495	. . 3 ⊢ (𝐺 ∈ TarskiGC → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦))
14	7, 13	syl 17	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦))
15		axtgcgrid.4	. 2 ⊢ (𝜑 → (𝑋 − 𝑌) = (𝑍 − 𝑍))
16		axtgcgrid.1	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
17		axtgcgrid.2	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
18		axtgcgrid.3	. . 3 ⊢ (𝜑 → 𝑍 ∈ 𝑃)
19		oveq1 7374	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦))
20	19	eqeq1d 2738	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑧 − 𝑧) ↔ (𝑋 − 𝑦) = (𝑧 − 𝑧)))
21		eqeq1 2740	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝑥 = 𝑦 ↔ 𝑋 = 𝑦))
22	20, 21	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) ↔ ((𝑋 − 𝑦) = (𝑧 − 𝑧) → 𝑋 = 𝑦)))
23		oveq2 7375	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌))
24	23	eqeq1d 2738	. . . . 5 ⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑧 − 𝑧) ↔ (𝑋 − 𝑌) = (𝑧 − 𝑧)))
25		eqeq2 2748	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑋 = 𝑦 ↔ 𝑋 = 𝑌))
26	24, 25	imbi12d 344	. . . 4 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑦) = (𝑧 − 𝑧) → 𝑋 = 𝑦) ↔ ((𝑋 − 𝑌) = (𝑧 − 𝑧) → 𝑋 = 𝑌)))
27		id 22	. . . . . . 7 ⊢ (𝑧 = 𝑍 → 𝑧 = 𝑍)
28	27, 27	oveq12d 7385	. . . . . 6 ⊢ (𝑧 = 𝑍 → (𝑧 − 𝑧) = (𝑍 − 𝑍))
29	28	eqeq2d 2747	. . . . 5 ⊢ (𝑧 = 𝑍 → ((𝑋 − 𝑌) = (𝑧 − 𝑧) ↔ (𝑋 − 𝑌) = (𝑍 − 𝑍)))
30	29	imbi1d 341	. . . 4 ⊢ (𝑧 = 𝑍 → (((𝑋 − 𝑌) = (𝑧 − 𝑧) → 𝑋 = 𝑌) ↔ ((𝑋 − 𝑌) = (𝑍 − 𝑍) → 𝑋 = 𝑌)))
31	22, 26, 30	rspc3v 3580	. . 3 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) → ((𝑋 − 𝑌) = (𝑍 − 𝑍) → 𝑋 = 𝑌)))
32	16, 17, 18, 31	syl3anc 1374	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) → ((𝑋 − 𝑌) = (𝑍 − 𝑍) → 𝑋 = 𝑌)))
33	14, 15, 32	mp2d 49	1 ⊢ (𝜑 → 𝑋 = 𝑌)

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  {cab 2714  ∀wral 3051  {crab 3389  Vcvv 3429  [wsbc 3728   ∖ cdif 3886   ∩ cin 3888  {csn 4567  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369  Basecbs 17179  distcds 17229  TarskiGcstrkg 28495  TarskiG_Ccstrkgc 28496  TarskiG_Bcstrkgb 28497  TarskiG_CBcstrkgcb 28498  Itvcitv 28501  LineGclng 28502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-trkgc 28516  df-trkg 28521

This theorem is referenced by:  tgcgreqb  28549  tgcgrtriv  28552  tgsegconeq  28554  tgbtwntriv2  28555  tgbtwndiff  28574  tgifscgr  28576  tgbtwnxfr  28598  lnid  28638  tgbtwnconn1lem2  28641  tgbtwnconn1lem3  28642  legtri3  28658  legeq  28661  legbtwn  28662  mirreu3  28722  colmid  28756  krippenlem  28758  lmiisolem  28864  hypcgrlem1  28867  hypcgrlem2  28868  f1otrg  28939