| Step | Hyp | Ref
| Expression |
| 1 | | dipfval.7 |
. 2
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
| 2 | | fveq2 6906 |
. . . . 5
⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = (BaseSet‘𝑈)) |
| 3 | | dipfval.1 |
. . . . 5
⊢ 𝑋 = (BaseSet‘𝑈) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . 4
⊢ (𝑢 = 𝑈 → (BaseSet‘𝑢) = 𝑋) |
| 5 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑈 → (normCV‘𝑢) =
(normCV‘𝑈)) |
| 6 | | dipfval.6 |
. . . . . . . . . 10
⊢ 𝑁 =
(normCV‘𝑈) |
| 7 | 5, 6 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝑢 = 𝑈 → (normCV‘𝑢) = 𝑁) |
| 8 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = ( +𝑣
‘𝑈)) |
| 9 | | dipfval.2 |
. . . . . . . . . . 11
⊢ 𝐺 = ( +𝑣
‘𝑈) |
| 10 | 8, 9 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = 𝐺) |
| 11 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑈 → 𝑥 = 𝑥) |
| 12 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑈 → (
·𝑠OLD ‘𝑢) = ( ·𝑠OLD
‘𝑈)) |
| 13 | | dipfval.4 |
. . . . . . . . . . . 12
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
| 14 | 12, 13 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑈 → (
·𝑠OLD ‘𝑢) = 𝑆) |
| 15 | 14 | oveqd 7448 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑈 → ((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦) = ((i↑𝑘)𝑆𝑦)) |
| 16 | 10, 11, 15 | oveq123d 7452 |
. . . . . . . . 9
⊢ (𝑢 = 𝑈 → (𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)) = (𝑥𝐺((i↑𝑘)𝑆𝑦))) |
| 17 | 7, 16 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑢 = 𝑈 → ((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦))) = (𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))) |
| 18 | 17 | oveq1d 7446 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2) = ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2)) |
| 19 | 18 | oveq2d 7447 |
. . . . . 6
⊢ (𝑢 = 𝑈 → ((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) = ((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2))) |
| 20 | 19 | sumeq2sdv 15739 |
. . . . 5
⊢ (𝑢 = 𝑈 → Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) = Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2))) |
| 21 | 20 | oveq1d 7446 |
. . . 4
⊢ (𝑢 = 𝑈 → (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) / 4) = (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2)) / 4)) |
| 22 | 4, 4, 21 | mpoeq123dv 7508 |
. . 3
⊢ (𝑢 = 𝑈 → (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) / 4)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2)) / 4))) |
| 23 | | df-dip 30720 |
. . 3
⊢
·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) / 4))) |
| 24 | 3 | fvexi 6920 |
. . . 4
⊢ 𝑋 ∈ V |
| 25 | 24, 24 | mpoex 8104 |
. . 3
⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2)) / 4)) ∈ V |
| 26 | 22, 23, 25 | fvmpt 7016 |
. 2
⊢ (𝑈 ∈ NrmCVec →
(·𝑖OLD‘𝑈) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2)) / 4))) |
| 27 | 1, 26 | eqtrid 2789 |
1
⊢ (𝑈 ∈ NrmCVec → 𝑃 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝑥𝐺((i↑𝑘)𝑆𝑦)))↑2)) / 4))) |