| Step | Hyp | Ref
| Expression |
| 1 | | nmpropd2.1 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
| 2 | | nmpropd2.2 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
| 3 | 1, 2 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) |
| 4 | | nmpropd2.5 |
. . . . . 6
⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) |
| 5 | 1 | sqxpeqd 5717 |
. . . . . . 7
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐾) × (Base‘𝐾))) |
| 6 | 5 | reseq2d 5997 |
. . . . . 6
⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) |
| 7 | 4, 6 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → ((dist‘𝐿) ↾ (𝐵 × 𝐵)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) |
| 8 | 2 | sqxpeqd 5717 |
. . . . . 6
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐿) × (Base‘𝐿))) |
| 9 | 8 | reseq2d 5997 |
. . . . 5
⊢ (𝜑 → ((dist‘𝐿) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))) |
| 10 | 7, 9 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) = ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))) |
| 11 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → 𝑎 = 𝑎) |
| 12 | | nmpropd2.4 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) |
| 13 | 1, 2, 12 | grpidpropd 18675 |
. . . 4
⊢ (𝜑 → (0g‘𝐾) = (0g‘𝐿)) |
| 14 | 10, 11, 13 | oveq123d 7452 |
. . 3
⊢ (𝜑 → (𝑎((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))(0g‘𝐾)) = (𝑎((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))(0g‘𝐿))) |
| 15 | 3, 14 | mpteq12dv 5233 |
. 2
⊢ (𝜑 → (𝑎 ∈ (Base‘𝐾) ↦ (𝑎((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))(0g‘𝐾))) = (𝑎 ∈ (Base‘𝐿) ↦ (𝑎((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))(0g‘𝐿)))) |
| 16 | | nmpropd2.3 |
. . 3
⊢ (𝜑 → 𝐾 ∈ Grp) |
| 17 | | eqid 2737 |
. . . 4
⊢
(norm‘𝐾) =
(norm‘𝐾) |
| 18 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 19 | | eqid 2737 |
. . . 4
⊢
(0g‘𝐾) = (0g‘𝐾) |
| 20 | | eqid 2737 |
. . . 4
⊢
(dist‘𝐾) =
(dist‘𝐾) |
| 21 | | eqid 2737 |
. . . 4
⊢
((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾))) =
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) |
| 22 | 17, 18, 19, 20, 21 | nmfval2 24604 |
. . 3
⊢ (𝐾 ∈ Grp →
(norm‘𝐾) = (𝑎 ∈ (Base‘𝐾) ↦ (𝑎((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))(0g‘𝐾)))) |
| 23 | 16, 22 | syl 17 |
. 2
⊢ (𝜑 → (norm‘𝐾) = (𝑎 ∈ (Base‘𝐾) ↦ (𝑎((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))(0g‘𝐾)))) |
| 24 | 1, 2, 12 | grppropd 18969 |
. . . 4
⊢ (𝜑 → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp)) |
| 25 | 16, 24 | mpbid 232 |
. . 3
⊢ (𝜑 → 𝐿 ∈ Grp) |
| 26 | | eqid 2737 |
. . . 4
⊢
(norm‘𝐿) =
(norm‘𝐿) |
| 27 | | eqid 2737 |
. . . 4
⊢
(Base‘𝐿) =
(Base‘𝐿) |
| 28 | | eqid 2737 |
. . . 4
⊢
(0g‘𝐿) = (0g‘𝐿) |
| 29 | | eqid 2737 |
. . . 4
⊢
(dist‘𝐿) =
(dist‘𝐿) |
| 30 | | eqid 2737 |
. . . 4
⊢
((dist‘𝐿)
↾ ((Base‘𝐿)
× (Base‘𝐿))) =
((dist‘𝐿) ↾
((Base‘𝐿) ×
(Base‘𝐿))) |
| 31 | 26, 27, 28, 29, 30 | nmfval2 24604 |
. . 3
⊢ (𝐿 ∈ Grp →
(norm‘𝐿) = (𝑎 ∈ (Base‘𝐿) ↦ (𝑎((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))(0g‘𝐿)))) |
| 32 | 25, 31 | syl 17 |
. 2
⊢ (𝜑 → (norm‘𝐿) = (𝑎 ∈ (Base‘𝐿) ↦ (𝑎((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))(0g‘𝐿)))) |
| 33 | 15, 23, 32 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿)) |