Theorem axtgcgrid

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

Proof

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