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