Theorem axtgcgrid 28397

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 28387	. . . . 5 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss1 4203	. . . . . 6 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩ TarskiGB)
3		inss1 4203	. . . . . 6 ⊢ (TarskiGC ∩ TarskiGB) ⊆ TarskiGC
4	2, 3	sstri 3959	. . . . 5 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGC
5	1, 4	eqsstri 3996	. . . 4 ⊢ TarskiG ⊆ TarskiGC
6		axtrkg.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sselid 3947	. . 3 ⊢ (𝜑 → 𝐺 ∈ TarskiGC)
8		axtrkg.p	. . . . . 6 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . 6 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . 6 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgc 28388	. . . . 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 7397	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 − 𝑦) = (𝑋 − 𝑦))
20	19	eqeq1d 2732	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 − 𝑦) = (𝑧 − 𝑧) ↔ (𝑋 − 𝑦) = (𝑧 − 𝑧)))
21		eqeq1 2734	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝑥 = 𝑦 ↔ 𝑋 = 𝑦))
22	20, 21	imbi12d 344	. . . 4 ⊢ (𝑥 = 𝑋 → (((𝑥 − 𝑦) = (𝑧 − 𝑧) → 𝑥 = 𝑦) ↔ ((𝑋 − 𝑦) = (𝑧 − 𝑧) → 𝑋 = 𝑦)))
23		oveq2 7398	. . . . . 6 ⊢ (𝑦 = 𝑌 → (𝑋 − 𝑦) = (𝑋 − 𝑌))
24	23	eqeq1d 2732	. . . . 5 ⊢ (𝑦 = 𝑌 → ((𝑋 − 𝑦) = (𝑧 − 𝑧) ↔ (𝑋 − 𝑌) = (𝑧 − 𝑧)))
25		eqeq2 2742	. . . . 5 ⊢ (𝑦 = 𝑌 → (𝑋 = 𝑦 ↔ 𝑋 = 𝑌))
26	24, 25	imbi12d 344	. . . 4 ⊢ (𝑦 = 𝑌 → (((𝑋 − 𝑦) = (𝑧 − 𝑧) → 𝑋 = 𝑦) ↔ ((𝑋 − 𝑌) = (𝑧 − 𝑧) → 𝑋 = 𝑌)))
27		id 22	. . . . . . 7 ⊢ (𝑧 = 𝑍 → 𝑧 = 𝑍)
28	27, 27	oveq12d 7408	. . . . . 6 ⊢ (𝑧 = 𝑍 → (𝑧 − 𝑧) = (𝑍 − 𝑍))
29	28	eqeq2d 2741	. . . . 5 ⊢ (𝑧 = 𝑍 → ((𝑋 − 𝑌) = (𝑧 − 𝑧) ↔ (𝑋 − 𝑌) = (𝑍 − 𝑍)))
30	29	imbi1d 341	. . . 4 ⊢ (𝑧 = 𝑍 → (((𝑋 − 𝑌) = (𝑧 − 𝑧) → 𝑋 = 𝑌) ↔ ((𝑋 − 𝑌) = (𝑍 − 𝑍) → 𝑋 = 𝑌)))
31	22, 26, 30	rspc3v 3607	. . 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 1540   ∈ wcel 2109  {cab 2708  ∀wral 3045  {crab 3408  Vcvv 3450  [wsbc 3756   ∖ cdif 3914   ∩ cin 3916  {csn 4592  ‘cfv 6514  (class class class)co 7390   ∈ cmpo 7392  Basecbs 17186  distcds 17236  TarskiGcstrkg 28361  TarskiG_Ccstrkgc 28362  TarskiG_Bcstrkgb 28363  TarskiG_CBcstrkgcb 28364  Itvcitv 28367  LineGclng 28368

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 2702  ax-nul 5264

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-trkgc 28382  df-trkg 28387

This theorem is referenced by:  tgcgreqb  28415  tgcgrtriv  28418  tgsegconeq  28420  tgbtwntriv2  28421  tgbtwndiff  28440  tgifscgr  28442  tgbtwnxfr  28464  lnid  28504  tgbtwnconn1lem2  28507  tgbtwnconn1lem3  28508  legtri3  28524  legeq  28527  legbtwn  28528  mirreu3  28588  colmid  28622  krippenlem  28624  lmiisolem  28730  hypcgrlem1  28733  hypcgrlem2  28734  f1otrg  28805