Step |
Hyp |
Ref |
Expression |
1 |
|
iscgrg.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
iscgrg.m |
⊢ − = ( dist ‘ 𝐺 ) |
3 |
|
iscgrg.e |
⊢ ∼ = ( cgrG ‘ 𝐺 ) |
4 |
|
elex |
⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ V ) |
5 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) ) |
6 |
5 1
|
eqtr4di |
⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝑃 ) |
7 |
6
|
oveq1d |
⊢ ( 𝑔 = 𝐺 → ( ( Base ‘ 𝑔 ) ↑pm ℝ ) = ( 𝑃 ↑pm ℝ ) ) |
8 |
7
|
eleq2d |
⊢ ( 𝑔 = 𝐺 → ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ↔ 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ) ) |
9 |
7
|
eleq2d |
⊢ ( 𝑔 = 𝐺 → ( 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ↔ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ) |
10 |
8 9
|
anbi12d |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ↔ ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ) ) |
11 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = ( dist ‘ 𝐺 ) ) |
12 |
11 2
|
eqtr4di |
⊢ ( 𝑔 = 𝐺 → ( dist ‘ 𝑔 ) = − ) |
13 |
12
|
oveqd |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) ) |
14 |
12
|
oveqd |
⊢ ( 𝑔 = 𝐺 → ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) |
15 |
13 14
|
eqeq12d |
⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ↔ ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) |
16 |
15
|
2ralbidv |
⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) |
17 |
16
|
anbi2d |
⊢ ( 𝑔 = 𝐺 → ( ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ↔ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) ) |
18 |
10 17
|
anbi12d |
⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) ) ) |
19 |
18
|
opabbidv |
⊢ ( 𝑔 = 𝐺 → { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) } = { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } ) |
20 |
|
df-cgrg |
⊢ cgrG = ( 𝑔 ∈ V ↦ { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) } ) |
21 |
|
df-xp |
⊢ ( ( 𝑃 ↑pm ℝ ) × ( 𝑃 ↑pm ℝ ) ) = { 〈 𝑎 , 𝑏 〉 ∣ ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) } |
22 |
|
ovex |
⊢ ( 𝑃 ↑pm ℝ ) ∈ V |
23 |
22 22
|
xpex |
⊢ ( ( 𝑃 ↑pm ℝ ) × ( 𝑃 ↑pm ℝ ) ) ∈ V |
24 |
21 23
|
eqeltrri |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) } ∈ V |
25 |
|
simpl |
⊢ ( ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) → ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ) |
26 |
25
|
ssopab2i |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } ⊆ { 〈 𝑎 , 𝑏 〉 ∣ ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) } |
27 |
24 26
|
ssexi |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } ∈ V |
28 |
19 20 27
|
fvmpt |
⊢ ( 𝐺 ∈ V → ( cgrG ‘ 𝐺 ) = { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } ) |
29 |
4 28
|
syl |
⊢ ( 𝐺 ∈ 𝑉 → ( cgrG ‘ 𝐺 ) = { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } ) |
30 |
3 29
|
syl5eq |
⊢ ( 𝐺 ∈ 𝑉 → ∼ = { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } ) |
31 |
30
|
breqd |
⊢ ( 𝐺 ∈ 𝑉 → ( 𝐴 ∼ 𝐵 ↔ 𝐴 { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } 𝐵 ) ) |
32 |
|
dmeq |
⊢ ( 𝑎 = 𝐴 → dom 𝑎 = dom 𝐴 ) |
33 |
32
|
eqeq1d |
⊢ ( 𝑎 = 𝐴 → ( dom 𝑎 = dom 𝑏 ↔ dom 𝐴 = dom 𝑏 ) ) |
34 |
32
|
adantr |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) → dom 𝑎 = dom 𝐴 ) |
35 |
|
simpll |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → 𝑎 = 𝐴 ) |
36 |
35
|
fveq1d |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → ( 𝑎 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) ) |
37 |
35
|
fveq1d |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → ( 𝑎 ‘ 𝑗 ) = ( 𝐴 ‘ 𝑗 ) ) |
38 |
36 37
|
oveq12d |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) ) |
39 |
38
|
eqeq1d |
⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) ∧ 𝑗 ∈ dom 𝑎 ) → ( ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) |
40 |
34 39
|
raleqbidva |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎 ) → ( ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) |
41 |
32 40
|
raleqbidva |
⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) |
42 |
33 41
|
anbi12d |
⊢ ( 𝑎 = 𝐴 → ( ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ↔ ( dom 𝐴 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) ) |
43 |
|
dmeq |
⊢ ( 𝑏 = 𝐵 → dom 𝑏 = dom 𝐵 ) |
44 |
43
|
eqeq2d |
⊢ ( 𝑏 = 𝐵 → ( dom 𝐴 = dom 𝑏 ↔ dom 𝐴 = dom 𝐵 ) ) |
45 |
|
fveq1 |
⊢ ( 𝑏 = 𝐵 → ( 𝑏 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) ) |
46 |
|
fveq1 |
⊢ ( 𝑏 = 𝐵 → ( 𝑏 ‘ 𝑗 ) = ( 𝐵 ‘ 𝑗 ) ) |
47 |
45 46
|
oveq12d |
⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) |
48 |
47
|
eqeq2d |
⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) |
49 |
48
|
2ralbidv |
⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ↔ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) |
50 |
44 49
|
anbi12d |
⊢ ( 𝑏 = 𝐵 → ( ( dom 𝐴 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ↔ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) ) |
51 |
42 50
|
sylan9bb |
⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ↔ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) ) |
52 |
|
eqid |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } = { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } |
53 |
51 52
|
brab2a |
⊢ ( 𝐴 { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑏 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) − ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) − ( 𝑏 ‘ 𝑗 ) ) ) ) } 𝐵 ↔ ( ( 𝐴 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝐵 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) ) |
54 |
31 53
|
bitrdi |
⊢ ( 𝐺 ∈ 𝑉 → ( 𝐴 ∼ 𝐵 ↔ ( ( 𝐴 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝐵 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝐴 = dom 𝐵 ∧ ∀ 𝑖 ∈ dom 𝐴 ∀ 𝑗 ∈ dom 𝐴 ( ( 𝐴 ‘ 𝑖 ) − ( 𝐴 ‘ 𝑗 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑗 ) ) ) ) ) ) |