| Step | Hyp | Ref
| Expression |
| 1 | | iscgrg.e |
. . . 4
⊢ ∼ =
(cgrG‘𝐺) |
| 2 | | elex 3501 |
. . . . 5
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
| 3 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
| 4 | | iscgrg.p |
. . . . . . . . . . . 12
⊢ 𝑃 = (Base‘𝐺) |
| 5 | 3, 4 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑃) |
| 6 | 5 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → ((Base‘𝑔) ↑pm ℝ) = (𝑃 ↑pm
ℝ)) |
| 7 | 6 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ↔ 𝑎 ∈ (𝑃 ↑pm
ℝ))) |
| 8 | 6 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑏 ∈ ((Base‘𝑔) ↑pm ℝ) ↔ 𝑏 ∈ (𝑃 ↑pm
ℝ))) |
| 9 | 7, 8 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ))
↔ (𝑎 ∈ (𝑃 ↑pm ℝ)
∧ 𝑏 ∈ (𝑃 ↑pm
ℝ)))) |
| 10 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = (dist‘𝐺)) |
| 11 | | iscgrg.m |
. . . . . . . . . . . . 13
⊢ − =
(dist‘𝐺) |
| 12 | 10, 11 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → (dist‘𝑔) = − ) |
| 13 | 12 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑎‘𝑖) − (𝑎‘𝑗))) |
| 14 | 12 | oveqd 7448 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) |
| 15 | 13, 14 | eqeq12d 2753 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) ↔ ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
| 16 | 15 | 2ralbidv 3221 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
| 17 | 16 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))) ↔ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))) |
| 18 | 9, 17 | anbi12d 632 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ))
∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗)))) ↔ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))))) |
| 19 | 18 | opabbidv 5209 |
. . . . . 6
⊢ (𝑔 = 𝐺 → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ) ∧ 𝑏 ∈ ((Base‘𝑔) ↑pm ℝ))
∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}) |
| 20 | | df-cgrg 28519 |
. . . . . 6
⊢ cgrG =
(𝑔 ∈ V ↦
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ ((Base‘𝑔) ↑pm ℝ)
∧ 𝑏 ∈
((Base‘𝑔)
↑pm ℝ)) ∧ (dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖)(dist‘𝑔)(𝑎‘𝑗)) = ((𝑏‘𝑖)(dist‘𝑔)(𝑏‘𝑗))))}) |
| 21 | | df-xp 5691 |
. . . . . . . 8
⊢ ((𝑃 ↑pm ℝ)
× (𝑃
↑pm ℝ)) = {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm
ℝ))} |
| 22 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑃 ↑pm ℝ)
∈ V |
| 23 | 22, 22 | xpex 7773 |
. . . . . . . 8
⊢ ((𝑃 ↑pm ℝ)
× (𝑃
↑pm ℝ)) ∈ V |
| 24 | 21, 23 | eqeltrri 2838 |
. . . . . . 7
⊢
{〈𝑎, 𝑏〉 ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))} ∈
V |
| 25 | | simpl 482 |
. . . . . . . 8
⊢ (((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) → (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm
ℝ))) |
| 26 | 25 | ssopab2i 5555 |
. . . . . . 7
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ⊆ {〈𝑎, 𝑏〉 ∣ (𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm
ℝ))} |
| 27 | 24, 26 | ssexi 5322 |
. . . . . 6
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} ∈ V |
| 28 | 19, 20, 27 | fvmpt 7016 |
. . . . 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 | eqtrid 2789 |
. . 3
⊢ (𝐺 ∈ 𝑉 → ∼ = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}) |
| 31 | 30 | breqd 5154 |
. 2
⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ 𝐴{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}𝐵)) |
| 32 | | dmeq 5914 |
. . . . . 6
⊢ (𝑎 = 𝐴 → dom 𝑎 = dom 𝐴) |
| 33 | 32 | eqeq1d 2739 |
. . . . 5
⊢ (𝑎 = 𝐴 → (dom 𝑎 = dom 𝑏 ↔ dom 𝐴 = dom 𝑏)) |
| 34 | 32 | adantr 480 |
. . . . . . 7
⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → dom 𝑎 = dom 𝐴) |
| 35 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → 𝑎 = 𝐴) |
| 36 | 35 | fveq1d 6908 |
. . . . . . . . 9
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑖) = (𝐴‘𝑖)) |
| 37 | 35 | fveq1d 6908 |
. . . . . . . . 9
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (𝑎‘𝑗) = (𝐴‘𝑗)) |
| 38 | 36, 37 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → ((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝐴‘𝑖) − (𝐴‘𝑗))) |
| 39 | 38 | eqeq1d 2739 |
. . . . . . 7
⊢ (((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) ∧ 𝑗 ∈ dom 𝑎) → (((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
| 40 | 34, 39 | raleqbidva 3332 |
. . . . . 6
⊢ ((𝑎 = 𝐴 ∧ 𝑖 ∈ dom 𝑎) → (∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
| 41 | 32, 40 | raleqbidva 3332 |
. . . . 5
⊢ (𝑎 = 𝐴 → (∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)))) |
| 42 | 33, 41 | anbi12d 632 |
. . . 4
⊢ (𝑎 = 𝐴 → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))) |
| 43 | | dmeq 5914 |
. . . . . 6
⊢ (𝑏 = 𝐵 → dom 𝑏 = dom 𝐵) |
| 44 | 43 | eqeq2d 2748 |
. . . . 5
⊢ (𝑏 = 𝐵 → (dom 𝐴 = dom 𝑏 ↔ dom 𝐴 = dom 𝐵)) |
| 45 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (𝑏‘𝑖) = (𝐵‘𝑖)) |
| 46 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (𝑏‘𝑗) = (𝐵‘𝑗)) |
| 47 | 45, 46 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → ((𝑏‘𝑖) − (𝑏‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))) |
| 48 | 47 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
| 49 | 48 | 2ralbidv 3221 |
. . . . 5
⊢ (𝑏 = 𝐵 → (∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗)) ↔ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))) |
| 50 | 44, 49 | anbi12d 632 |
. . . 4
⊢ (𝑏 = 𝐵 → ((dom 𝐴 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
| 51 | 42, 50 | sylan9bb 509 |
. . 3
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → ((dom 𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
| 52 | | eqid 2737 |
. . 3
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))} |
| 53 | 51, 52 | brab2a 5779 |
. 2
⊢ (𝐴{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝑎 = dom 𝑏 ∧ ∀𝑖 ∈ dom 𝑎∀𝑗 ∈ dom 𝑎((𝑎‘𝑖) − (𝑎‘𝑗)) = ((𝑏‘𝑖) − (𝑏‘𝑗))))}𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗))))) |
| 54 | 31, 53 | bitrdi 287 |
1
⊢ (𝐺 ∈ 𝑉 → (𝐴 ∼ 𝐵 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐵 ∈ (𝑃 ↑pm ℝ)) ∧ (dom
𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴∀𝑗 ∈ dom 𝐴((𝐴‘𝑖) − (𝐴‘𝑗)) = ((𝐵‘𝑖) − (𝐵‘𝑗)))))) |