Theorem axtgcgrid 28447

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 28437	. . . . 5 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss1 4186	. . . . . 6 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩ TarskiGB)
3		inss1 4186	. . . . . 6 ⊢ (TarskiGC ∩ TarskiGB) ⊆ TarskiGC
4	2, 3	sstri 3939	. . . . 5 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGC
5	1, 4	eqsstri 3976	. . . 4 ⊢ TarskiG ⊆ TarskiGC
6		axtrkg.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sselid 3927	. . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiGC)
8		axtrkg.p	. . . . . 6 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . 6 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . 6 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgc 28438	. . . . 5 ⊢ (𝐺 ∈ TarskiGC ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 − 𝑦) = (𝑦 − 𝑥) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦))))
12	11	simprbi 496	. . . 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 7359	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦))
20	19	eqeq1d 2733	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑧 − 𝑧) ↔ (𝑋 − 𝑦) = (𝑧 − 𝑧)))
21		eqeq1 2735	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝑥 = 𝑦 ↔ 𝑋 = 𝑦))
22	20, 21	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) ↔ ((𝑋 − 𝑦) = (𝑧 − 𝑧) → 𝑋 = 𝑦)))
23		oveq2 7360	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌))
24	23	eqeq1d 2733	. . . . 5 ⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑧 − 𝑧) ↔ (𝑋 − 𝑌) = (𝑧 − 𝑧)))
25		eqeq2 2743	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑋 = 𝑦 ↔ 𝑋 = 𝑌))
26	24, 25	imbi12d 344	. . . 4 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑦) = (𝑧 − 𝑧) → 𝑋 = 𝑦) ↔ ((𝑋 − 𝑌) = (𝑧 − 𝑧) → 𝑋 = 𝑌)))
27		id 22	. . . . . . 7 ⊢ (𝑧 = 𝑍 → 𝑧 = 𝑍)
28	27, 27	oveq12d 7370	. . . . . 6 ⊢ (𝑧 = 𝑍 → (𝑧 − 𝑧) = (𝑍 − 𝑍))
29	28	eqeq2d 2742	. . . . 5 ⊢ (𝑧 = 𝑍 → ((𝑋 − 𝑌) = (𝑧 − 𝑧) ↔ (𝑋 − 𝑌) = (𝑍 − 𝑍)))
30	29	imbi1d 341	. . . 4 ⊢ (𝑧 = 𝑍 → (((𝑋 − 𝑌) = (𝑧 − 𝑧) → 𝑋 = 𝑌) ↔ ((𝑋 − 𝑌) = (𝑍 − 𝑍) → 𝑋 = 𝑌)))
31	22, 26, 30	rspc3v 3588	. . 3 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) → ((𝑋 − 𝑌) = (𝑍 − 𝑍) → 𝑋 = 𝑌)))
32	16, 17, 18, 31	syl3anc 1373	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) → ((𝑋 − 𝑌) = (𝑍 − 𝑍) → 𝑋 = 𝑌)))
33	14, 15, 32	mp2d 49	1 ⊢ (𝜑 → 𝑋 = 𝑌)

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085   = wceq 1541   ∈ wcel 2111  {cab 2709  ∀wral 3047  {crab 3395  Vcvv 3436  [wsbc 3736   ∖ cdif 3894   ∩ cin 3896  {csn 4575  ‘cfv 6487  (class class class)co 7352   ∈ cmpo 7354  Basecbs 17126  distcds 17176  TarskiGcstrkg 28411  TarskiG_Ccstrkgc 28412  TarskiG_Bcstrkgb 28413  TarskiG_CBcstrkgcb 28414  Itvcitv 28417  LineGclng 28418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6443  df-fv 6495  df-ov 7355  df-trkgc 28432  df-trkg 28437

This theorem is referenced by:  tgcgreqb  28465  tgcgrtriv  28468  tgsegconeq  28470  tgbtwntriv2  28471  tgbtwndiff  28490  tgifscgr  28492  tgbtwnxfr  28514  lnid  28554  tgbtwnconn1lem2  28557  tgbtwnconn1lem3  28558  legtri3  28574  legeq  28577  legbtwn  28578  mirreu3  28638  colmid  28672  krippenlem  28674  lmiisolem  28780  hypcgrlem1  28783  hypcgrlem2  28784  f1otrg  28855