Metamath Proof Explorer

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 4 eqcomd ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → 𝑃 = 𝑝 )
6 5 adantr ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) → 𝑃 = 𝑝 )
7 simpllr ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑑 = − )
8 7 eqcomd ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → − = 𝑑 )
9 8 oveqd ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( 𝑥 − 𝑦 ) = ( 𝑥 𝑑 𝑦 ) )
10 8 oveqd ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( 𝑦 − 𝑥 ) = ( 𝑦 𝑑 𝑥 ) )
11 9 10 eqeq12d ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ↔ ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ) )
12 6 11 raleqbidva ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) → ( ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ) )
13 5 12 raleqbidva ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ) )
14 6 adantr ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → 𝑃 = 𝑝 )
15 8 oveqdr ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑥 − 𝑦 ) = ( 𝑥 𝑑 𝑦 ) )
16 8 oveqdr ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( 𝑧 − 𝑧 ) = ( 𝑧 𝑑 𝑧 ) )
17 15 16 eqeq12d ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) ↔ ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) ) )
18 17 imbi1d ⊢ ( ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑧 ∈ 𝑃 ) → ( ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) )
19 14 18 raleqbidva ⊢ ( ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑦 ∈ 𝑃 ) → ( ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) )
20 6 19 raleqbidva ⊢ ( ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) ∧ 𝑥 ∈ 𝑃 ) → ( ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) )
21 5 20 raleqbidva ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) )
22 13 21 anbi12d ⊢ ( ( 𝑝 = 𝑃 ∧ 𝑑 = − ) → ( ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) ) )
23 1 2 22 sbcie2s ⊢ ( 𝑓 = 𝐺 → ( [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) ) )
24 df-trkgc ⊢ TarskiGC = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( dist ‘ 𝑓 ) / 𝑑 ] ( ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ( 𝑥 𝑑 𝑦 ) = ( 𝑦 𝑑 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑝 ∀ 𝑦 ∈ 𝑝 ∀ 𝑧 ∈ 𝑝 ( ( 𝑥 𝑑 𝑦 ) = ( 𝑧 𝑑 𝑧 ) → 𝑥 = 𝑦 ) ) }
25 23 24 elab4g ⊢ ( 𝐺 ∈ TarskiGC ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 − 𝑦 ) = ( 𝑦 − 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ( 𝑥 − 𝑦 ) = ( 𝑧 − 𝑧 ) → 𝑥 = 𝑦 ) ) ) )