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 e. TarskiG -> ( cgrG ` G ) Er ( P ^pm RR ) )

Proof

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