Metamath Proof Explorer


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 P = Base G
axtrkg.d - ˙ = dist G
axtrkg.i I = Itv G
axtrkg.g φ G 𝒢 Tarski
axtgcgrid.1 φ X P
axtgcgrid.2 φ Y P
axtgcgrid.3 φ Z P
axtgcgrid.4 φ X - ˙ Y = Z - ˙ Z
Assertion axtgcgrid φ X = Y

Proof

Step Hyp Ref Expression
1 axtrkg.p P = Base G
2 axtrkg.d - ˙ = dist G
3 axtrkg.i I = Itv G
4 axtrkg.g φ G 𝒢 Tarski
5 axtgcgrid.1 φ X P
6 axtgcgrid.2 φ Y P
7 axtgcgrid.3 φ Z P
8 axtgcgrid.4 φ X - ˙ Y = Z - ˙ Z
9 df-trkg 𝒢 Tarski = 𝒢 Tarski C 𝒢 Tarski B 𝒢 Tarski CB f | [˙Base f / p]˙ [˙ Itv f / i]˙ Line 𝒢 f = x p , y p x z p | z x i y x z i y y x i z
10 inss1 𝒢 Tarski C 𝒢 Tarski B 𝒢 Tarski CB f | [˙Base f / p]˙ [˙ Itv f / i]˙ Line 𝒢 f = x p , y p x z p | z x i y x z i y y x i z 𝒢 Tarski C 𝒢 Tarski B
11 inss1 𝒢 Tarski C 𝒢 Tarski B 𝒢 Tarski C
12 10 11 sstri 𝒢 Tarski C 𝒢 Tarski B 𝒢 Tarski CB f | [˙Base f / p]˙ [˙ Itv f / i]˙ Line 𝒢 f = x p , y p x z p | z x i y x z i y y x i z 𝒢 Tarski C
13 9 12 eqsstri 𝒢 Tarski 𝒢 Tarski C
14 13 4 sseldi φ G 𝒢 Tarski C
15 1 2 3 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
16 15 simprbi G 𝒢 Tarski C x P y P x - ˙ y = y - ˙ x x P y P z P x - ˙ y = z - ˙ z x = y
17 16 simprd G 𝒢 Tarski C x P y P z P x - ˙ y = z - ˙ z x = y
18 14 17 syl φ x P y P z P x - ˙ y = z - ˙ z x = y
19 oveq1 x = X x - ˙ y = X - ˙ y
20 19 eqeq1d x = X x - ˙ y = z - ˙ z X - ˙ y = z - ˙ z
21 eqeq1 x = X x = y X = y
22 20 21 imbi12d x = X x - ˙ y = z - ˙ z x = y X - ˙ y = z - ˙ z X = y
23 oveq2 y = Y X - ˙ y = X - ˙ Y
24 23 eqeq1d y = Y X - ˙ y = z - ˙ z X - ˙ Y = z - ˙ z
25 eqeq2 y = Y X = y X = Y
26 24 25 imbi12d y = Y X - ˙ y = z - ˙ z X = y X - ˙ Y = z - ˙ z X = Y
27 id z = Z z = Z
28 27 27 oveq12d z = Z z - ˙ z = Z - ˙ Z
29 28 eqeq2d z = Z X - ˙ Y = z - ˙ z X - ˙ Y = Z - ˙ Z
30 29 imbi1d z = Z X - ˙ Y = z - ˙ z X = Y X - ˙ Y = Z - ˙ Z X = Y
31 22 26 30 rspc3v X P Y P Z P x P y P z P x - ˙ y = z - ˙ z x = y X - ˙ Y = Z - ˙ Z X = Y
32 5 6 7 31 syl3anc φ x P y P z P x - ˙ y = z - ˙ z x = y X - ˙ Y = Z - ˙ Z X = Y
33 18 8 32 mp2d φ X = Y