Metamath Proof Explorer


Theorem ercgrg

Description: The shape congruence relation is an equivalence relation. Statement 4.4 of Schwabhauser p. 35. (Contributed by Thierry Arnoux, 9-Apr-2019)

Ref Expression
Hypothesis ercgrg.p P = Base G
Assertion ercgrg G 𝒢 Tarski 𝒢 G Er P 𝑝𝑚

Proof

Step Hyp Ref Expression
1 ercgrg.p P = Base G
2 df-cgrg 𝒢 = g V a b | a Base g 𝑝𝑚 b Base g 𝑝𝑚 dom a = dom b i dom a j dom a a i dist g a j = b i dist g b j
3 2 relmptopab Rel 𝒢 G
4 3 a1i G 𝒢 Tarski Rel 𝒢 G
5 eqid dist G = dist G
6 eqid 𝒢 G = 𝒢 G
7 1 5 6 iscgrg G 𝒢 Tarski x 𝒢 G y x P 𝑝𝑚 y P 𝑝𝑚 dom x = dom y i dom x j dom x x i dist G x j = y i dist G y j
8 7 biimpa G 𝒢 Tarski x 𝒢 G y x P 𝑝𝑚 y P 𝑝𝑚 dom x = dom y i dom x j dom x x i dist G x j = y i dist G y j
9 8 simpld G 𝒢 Tarski x 𝒢 G y x P 𝑝𝑚 y P 𝑝𝑚
10 9 ancomd G 𝒢 Tarski x 𝒢 G y y P 𝑝𝑚 x P 𝑝𝑚
11 8 simprd G 𝒢 Tarski x 𝒢 G y dom x = dom y i dom x j dom x x i dist G x j = y i dist G y j
12 11 simpld G 𝒢 Tarski x 𝒢 G y dom x = dom y
13 12 eqcomd G 𝒢 Tarski x 𝒢 G y dom y = dom x
14 simpl G 𝒢 Tarski x 𝒢 G y i dom y j dom y G 𝒢 Tarski x 𝒢 G y
15 simprl G 𝒢 Tarski x 𝒢 G y i dom y j dom y i dom y
16 12 adantr G 𝒢 Tarski x 𝒢 G y i dom y j dom y dom x = dom y
17 15 16 eleqtrrd G 𝒢 Tarski x 𝒢 G y i dom y j dom y i dom x
18 simprr G 𝒢 Tarski x 𝒢 G y i dom y j dom y j dom y
19 18 16 eleqtrrd G 𝒢 Tarski x 𝒢 G y i dom y j dom y j dom x
20 11 simprd G 𝒢 Tarski x 𝒢 G y i dom x j dom x x i dist G x j = y i dist G y j
21 20 r19.21bi G 𝒢 Tarski x 𝒢 G y i dom x j dom x x i dist G x j = y i dist G y j
22 21 r19.21bi G 𝒢 Tarski x 𝒢 G y i dom x j dom x x i dist G x j = y i dist G y j
23 14 17 19 22 syl21anc G 𝒢 Tarski x 𝒢 G y i dom y j dom y x i dist G x j = y i dist G y j
24 23 eqcomd G 𝒢 Tarski x 𝒢 G y i dom y j dom y y i dist G y j = x i dist G x j
25 24 ralrimivva G 𝒢 Tarski x 𝒢 G y i dom y j dom y y i dist G y j = x i dist G x j
26 13 25 jca G 𝒢 Tarski x 𝒢 G y dom y = dom x i dom y j dom y y i dist G y j = x i dist G x j
27 1 5 6 iscgrg G 𝒢 Tarski y 𝒢 G x y P 𝑝𝑚 x P 𝑝𝑚 dom y = dom x i dom y j dom y y i dist G y j = x i dist G x j
28 27 adantr G 𝒢 Tarski x 𝒢 G y y 𝒢 G x y P 𝑝𝑚 x P 𝑝𝑚 dom y = dom x i dom y j dom y y i dist G y j = x i dist G x j
29 10 26 28 mpbir2and G 𝒢 Tarski x 𝒢 G y y 𝒢 G x
30 9 simpld G 𝒢 Tarski x 𝒢 G y x P 𝑝𝑚
31 30 adantrr G 𝒢 Tarski x 𝒢 G y y 𝒢 G z x P 𝑝𝑚
32 1 5 6 iscgrg G 𝒢 Tarski y 𝒢 G z y P 𝑝𝑚 z P 𝑝𝑚 dom y = dom z i dom y j dom y y i dist G y j = z i dist G z j
33 32 biimpa G 𝒢 Tarski y 𝒢 G z y P 𝑝𝑚 z P 𝑝𝑚 dom y = dom z i dom y j dom y y i dist G y j = z i dist G z j
34 33 adantrl G 𝒢 Tarski x 𝒢 G y y 𝒢 G z y P 𝑝𝑚 z P 𝑝𝑚 dom y = dom z i dom y j dom y y i dist G y j = z i dist G z j
35 34 simpld G 𝒢 Tarski x 𝒢 G y y 𝒢 G z y P 𝑝𝑚 z P 𝑝𝑚
36 35 simprd G 𝒢 Tarski x 𝒢 G y y 𝒢 G z z P 𝑝𝑚
37 31 36 jca G 𝒢 Tarski x 𝒢 G y y 𝒢 G z x P 𝑝𝑚 z P 𝑝𝑚
38 8 adantrr G 𝒢 Tarski x 𝒢 G y y 𝒢 G z x P 𝑝𝑚 y P 𝑝𝑚 dom x = dom y i dom x j dom x x i dist G x j = y i dist G y j
39 38 simprd G 𝒢 Tarski x 𝒢 G y y 𝒢 G z dom x = dom y i dom x j dom x x i dist G x j = y i dist G y j
40 39 simpld G 𝒢 Tarski x 𝒢 G y y 𝒢 G z dom x = dom y
41 34 simprd G 𝒢 Tarski x 𝒢 G y y 𝒢 G z dom y = dom z i dom y j dom y y i dist G y j = z i dist G z j
42 41 simpld G 𝒢 Tarski x 𝒢 G y y 𝒢 G z dom y = dom z
43 40 42 eqtrd G 𝒢 Tarski x 𝒢 G y y 𝒢 G z dom x = dom z
44 39 simprd G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x x i dist G x j = y i dist G y j
45 44 r19.21bi G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x x i dist G x j = y i dist G y j
46 45 r19.21bi G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x x i dist G x j = y i dist G y j
47 46 anasss G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x x i dist G x j = y i dist G y j
48 simpl G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x G 𝒢 Tarski x 𝒢 G y y 𝒢 G z
49 simprl G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x i dom x
50 40 adantr G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x dom x = dom y
51 49 50 eleqtrd G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x i dom y
52 simprr G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x j dom x
53 52 50 eleqtrd G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x j dom y
54 41 simprd G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom y j dom y y i dist G y j = z i dist G z j
55 54 r19.21bi G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom y j dom y y i dist G y j = z i dist G z j
56 55 r19.21bi G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom y j dom y y i dist G y j = z i dist G z j
57 48 51 53 56 syl21anc G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x y i dist G y j = z i dist G z j
58 47 57 eqtrd G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x x i dist G x j = z i dist G z j
59 58 ralrimivva G 𝒢 Tarski x 𝒢 G y y 𝒢 G z i dom x j dom x x i dist G x j = z i dist G z j
60 43 59 jca G 𝒢 Tarski x 𝒢 G y y 𝒢 G z dom x = dom z i dom x j dom x x i dist G x j = z i dist G z j
61 1 5 6 iscgrg G 𝒢 Tarski x 𝒢 G z x P 𝑝𝑚 z P 𝑝𝑚 dom x = dom z i dom x j dom x x i dist G x j = z i dist G z j
62 61 adantr G 𝒢 Tarski x 𝒢 G y y 𝒢 G z x 𝒢 G z x P 𝑝𝑚 z P 𝑝𝑚 dom x = dom z i dom x j dom x x i dist G x j = z i dist G z j
63 37 60 62 mpbir2and G 𝒢 Tarski x 𝒢 G y y 𝒢 G z x 𝒢 G z
64 pm4.24 x P 𝑝𝑚 x P 𝑝𝑚 x P 𝑝𝑚
65 eqid dom x = dom x
66 eqidd i dom x j dom x x i dist G x j = x i dist G x j
67 66 rgen2 i dom x j dom x x i dist G x j = x i dist G x j
68 65 67 pm3.2i dom x = dom x i dom x j dom x x i dist G x j = x i dist G x j
69 68 biantru x P 𝑝𝑚 x P 𝑝𝑚 x P 𝑝𝑚 x P 𝑝𝑚 dom x = dom x i dom x j dom x x i dist G x j = x i dist G x j
70 64 69 bitri x P 𝑝𝑚 x P 𝑝𝑚 x P 𝑝𝑚 dom x = dom x i dom x j dom x x i dist G x j = x i dist G x j
71 1 5 6 iscgrg G 𝒢 Tarski x 𝒢 G x x P 𝑝𝑚 x P 𝑝𝑚 dom x = dom x i dom x j dom x x i dist G x j = x i dist G x j
72 70 71 bitr4id G 𝒢 Tarski x P 𝑝𝑚 x 𝒢 G x
73 4 29 63 72 iserd G 𝒢 Tarski 𝒢 G Er P 𝑝𝑚