Step | Hyp | Ref
| Expression |
1 | | iscgrg.e |
. . . 4
⊢ ∼ =
(cgrG‘𝐺) |
2 | | elex 3185 |
. . . . 5
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
3 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
4 | | iscgrg.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (Base‘𝐺) |
5 | 3, 4 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) |
6 | 5 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((Base‘𝑔) ↑pm ℝ) =
(𝑃
↑pm ℝ)) |
7 | 6 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ↔
𝑎 ∈ (𝑃 ↑pm
ℝ))) |
8 | 6 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑏 ∈ ((Base‘𝑔) ↑pm ℝ) ↔
𝑏 ∈ (𝑃 ↑pm
ℝ))) |
9 | 7, 8 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧
𝑏 ∈ ((Base‘𝑔) ↑pm
ℝ)) ↔ (𝑎 ∈
(𝑃
↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm
ℝ)))) |
10 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = (dist‘𝐺)) |
11 | | iscgrg.m |
. . . . . . . . . . . . 13
⊢ − =
(dist‘𝐺) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = − ) |
13 | 12 | oveqd 6566 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑎‘𝑖) − (𝑎‘𝑗))) |
14 | 12 | oveqd 6566 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) |
15 | 13, 14 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) ↔ ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
16 | 15 | 2ralbidv 2972 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
17 | 16 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))) ↔ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))) |
18 | 9, 17 | anbi12d 743 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧
𝑏 ∈ ((Base‘𝑔) ↑pm
ℝ)) ∧ (dom 𝑎 =
dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)))) ↔ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))))) |
19 | 18 | opabbidv 4648 |
. . . . . 6
⊢ (𝑔 = 𝐺 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧
𝑏 ∈ ((Base‘𝑔) ↑pm
ℝ)) ∧ (dom 𝑎 =
dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}) |
20 | | df-cgrg 25206 |
. . . . . 6
⊢ cgrG =
(𝑔 ∈ V ↦
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm
ℝ) ∧ 𝑏 ∈
((Base‘𝑔)
↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))}) |
21 | | df-xp 5044 |
. . . . . . . 8
⊢ ((𝑃 ↑pm
ℝ) × (𝑃
↑pm ℝ)) = {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm
ℝ))} |
22 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑃 ↑pm
ℝ) ∈ V |
23 | 22, 22 | xpex 6860 |
. . . . . . . 8
⊢ ((𝑃 ↑pm
ℝ) × (𝑃
↑pm ℝ)) ∈ V |
24 | 21, 23 | eqeltrri 2685 |
. . . . . . 7
⊢
{〈𝑎, 𝑏〉 ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ))}
∈ V |
25 | | simpl 472 |
. . . . . . . 8
⊢ (((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) → (𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm
ℝ))) |
26 | 25 | ssopab2i 4928 |
. . . . . . 7
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ⊆ {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm
ℝ))} |
27 | 24, 26 | ssexi 4731 |
. . . . . 6
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ∈ V |
28 | 19, 20, 27 | fvmpt 6191 |
. . . . 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 2656 |
. . 3
⊢ (𝐺 ∈ 𝑉 → ∼ = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}) |
31 | 30 | breqd 4594 |
. 2
⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ 𝐴{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}𝐵)) |
32 | | dmeq 5246 |
. . . . . 6
⊢ (𝑎 = 𝐴 → dom 𝑎 = dom 𝐴) |
33 | 32 | eqeq1d 2612 |
. . . . 5
⊢ (𝑎 = 𝐴 → (dom 𝑎 = dom 𝑏 ↔ dom 𝐴 = dom 𝑏)) |
34 | 32 | adantr 480 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → dom 𝑎 = dom 𝐴) |
35 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → 𝑎 = 𝐴) |
36 | 35 | fveq1d 6105 |
. . . . . . . . 9
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑖) = (𝐴‘𝑖)) |
37 | 35 | fveq1d 6105 |
. . . . . . . . 9
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑗) = (𝐴‘𝑗)) |
38 | 36, 37 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝐴‘𝑖) − (𝐴‘𝑗))) |
39 | 38 | eqeq1d 2612 |
. . . . . . 7
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
40 | 34, 39 | raleqbidva 3131 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → (∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
41 | 32, 40 | raleqbidva 3131 |
. . . . 5
⊢ (𝑎 = 𝐴 → (∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
42 | 33, 41 | anbi12d 743 |
. . . 4
⊢ (𝑎 = 𝐴 → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))) |
43 | | dmeq 5246 |
. . . . . 6
⊢ (𝑏 = 𝐵 → dom 𝑏 = dom 𝐵) |
44 | 43 | eqeq2d 2620 |
. . . . 5
⊢ (𝑏 = 𝐵 → (dom 𝐴 = dom 𝑏 ↔ dom 𝐴 = dom 𝐵)) |
45 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (𝑏‘𝑖) = (𝐵‘𝑖)) |
46 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (𝑏‘𝑗) = (𝐵‘𝑗)) |
47 | 45, 46 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → ((𝑏‘𝑖) − (𝑏‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
48 | 47 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
49 | 48 | 2ralbidv 2972 |
. . . . 5
⊢ (𝑏 = 𝐵 → (∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
50 | 44, 49 | anbi12d 743 |
. . . 4
⊢ (𝑏 = 𝐵 → ((dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
51 | 42, 50 | sylan9bb 732 |
. . 3
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
52 | | eqid 2610 |
. . 3
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} |
53 | 51, 52 | brab2a 5091 |
. 2
⊢ (𝐴{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧
𝑏 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧
𝐵 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
54 | 31, 53 | syl6bb 275 |
1
⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧
𝐵 ∈ (𝑃 ↑pm ℝ)) ∧
(dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))) |