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 P = Base G
istrkg.d - ˙ = dist G
istrkg.i I = Itv G
Assertion istrkgc G 𝒢 Tarski C G V x P y P x - ˙ y = y - ˙ x x P y P z P x - ˙ y = z - ˙ z x = y

Proof

Step Hyp Ref Expression
1 istrkg.p P = Base G
2 istrkg.d - ˙ = dist G
3 istrkg.i I = Itv G
4 simpl p = P d = - ˙ p = P
5 simpr p = P d = - ˙ d = - ˙
6 5 oveqd p = P d = - ˙ x d y = x - ˙ y
7 5 oveqd p = P d = - ˙ y d x = y - ˙ x
8 6 7 eqeq12d p = P d = - ˙ x d y = y d x x - ˙ y = y - ˙ x
9 4 8 raleqbidv p = P d = - ˙ y p x d y = y d x y P x - ˙ y = y - ˙ x
10 4 9 raleqbidv p = P d = - ˙ x p y p x d y = y d x x P y P x - ˙ y = y - ˙ x
11 5 oveqd p = P d = - ˙ z d z = z - ˙ z
12 6 11 eqeq12d p = P d = - ˙ x d y = z d z x - ˙ y = z - ˙ z
13 12 imbi1d p = P d = - ˙ x d y = z d z x = y x - ˙ y = z - ˙ z x = y
14 4 13 raleqbidv p = P d = - ˙ z p x d y = z d z x = y z P x - ˙ y = z - ˙ z x = y
15 4 14 raleqbidv p = P d = - ˙ y p z p x d y = z d z x = y y P z P x - ˙ y = z - ˙ z x = y
16 4 15 raleqbidv p = P d = - ˙ x p y p z p x d y = z d z x = y x P y P z P x - ˙ y = z - ˙ z x = y
17 10 16 anbi12d p = P d = - ˙ x p y p x d y = y d x x p y p z p x d y = z d z x = y x P y P x - ˙ y = y - ˙ x x P y P z P x - ˙ y = z - ˙ z x = y
18 1 2 17 sbcie2s f = G [˙Base f / p]˙ [˙ dist f / d]˙ x p y p x d y = y d x x p y p z p x d y = z d z x = y x P y P x - ˙ y = y - ˙ x x P y P z P x - ˙ y = z - ˙ z x = y
19 df-trkgc 𝒢 Tarski C = f | [˙Base f / p]˙ [˙ dist f / d]˙ x p y p x d y = y d x x p y p z p x d y = z d z x = y
20 18 19 elab4g G 𝒢 Tarski C G V x P y P x - ˙ y = y - ˙ x x P y P z P x - ˙ y = z - ˙ z x = y