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