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 ) )