Theorem istrkgc

Description: Property of being a Tarski geometry - congruence part. (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	istrkg.d	⊢ − = ( dist ‘ 𝐺 )
	istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
Assertion	istrkgc	⊢ ( 𝐺 ∈ TarskiGC ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		istrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		istrkg.d	⊢ − = ( dist ‘ 𝐺 )
3		istrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		simpl	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → 𝑝 = 𝑃 )
5		simpr	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → 𝑑 = − )
6	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( 𝑥 𝑑 𝑦 ) = ( 𝑥 − 𝑦 ) )
7	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( 𝑦 𝑑 𝑥 ) = ( 𝑦 − 𝑥 ) )
8	6 7	eqeq12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ↔ ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ) )
9	4 8	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ) )
10	4 9	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ) )
11	5	oveqd	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( 𝑧 𝑑 𝑧 ) = ( 𝑧 − 𝑧 ) )
12	6 11	eqeq12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) ↔ ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) ) )
13	12	imbi1d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) )
14	4 13	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) )
15	4 14	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) )
16	4 15	raleqbidv	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) )
17	10 16	anbi12d	⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) ) )
18	1 2 17	sbcie2s	⊢ ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) ) )
19		df-trkgc	⊢ TarskiGC = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) }
20	18 19	elab4g	⊢ ( 𝐺 ∈ TarskiGC ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) ) )