Step | Hyp | Ref
| Expression |
1 | | dipfval.7 |
. 2
β’ π =
(Β·πOLDβπ) |
2 | | fveq2 6839 |
. . . . 5
β’ (π’ = π β (BaseSetβπ’) = (BaseSetβπ)) |
3 | | dipfval.1 |
. . . . 5
β’ π = (BaseSetβπ) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
β’ (π’ = π β (BaseSetβπ’) = π) |
5 | | fveq2 6839 |
. . . . . . . . . 10
β’ (π’ = π β (normCVβπ’) =
(normCVβπ)) |
6 | | dipfval.6 |
. . . . . . . . . 10
β’ π =
(normCVβπ) |
7 | 5, 6 | eqtr4di 2795 |
. . . . . . . . 9
β’ (π’ = π β (normCVβπ’) = π) |
8 | | fveq2 6839 |
. . . . . . . . . . 11
β’ (π’ = π β ( +π£ βπ’) = ( +π£
βπ)) |
9 | | dipfval.2 |
. . . . . . . . . . 11
β’ πΊ = ( +π£
βπ) |
10 | 8, 9 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π’ = π β ( +π£ βπ’) = πΊ) |
11 | | eqidd 2738 |
. . . . . . . . . 10
β’ (π’ = π β π₯ = π₯) |
12 | | fveq2 6839 |
. . . . . . . . . . . 12
β’ (π’ = π β (
Β·π OLD βπ’) = ( Β·π OLD
βπ)) |
13 | | dipfval.4 |
. . . . . . . . . . . 12
β’ π = (
Β·π OLD βπ) |
14 | 12, 13 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ (π’ = π β (
Β·π OLD βπ’) = π) |
15 | 14 | oveqd 7368 |
. . . . . . . . . 10
β’ (π’ = π β ((iβπ)( Β·π OLD
βπ’)π¦) = ((iβπ)ππ¦)) |
16 | 10, 11, 15 | oveq123d 7372 |
. . . . . . . . 9
β’ (π’ = π β (π₯( +π£ βπ’)((iβπ)( Β·π OLD
βπ’)π¦)) = (π₯πΊ((iβπ)ππ¦))) |
17 | 7, 16 | fveq12d 6846 |
. . . . . . . 8
β’ (π’ = π β ((normCVβπ’)β(π₯( +π£ βπ’)((iβπ)( Β·π OLD
βπ’)π¦))) = (πβ(π₯πΊ((iβπ)ππ¦)))) |
18 | 17 | oveq1d 7366 |
. . . . . . 7
β’ (π’ = π β (((normCVβπ’)β(π₯( +π£ βπ’)((iβπ)( Β·π OLD
βπ’)π¦)))β2) = ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) |
19 | 18 | oveq2d 7367 |
. . . . . 6
β’ (π’ = π β ((iβπ) Β· (((normCVβπ’)β(π₯( +π£ βπ’)((iβπ)( Β·π OLD
βπ’)π¦)))β2)) = ((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2))) |
20 | 19 | sumeq2sdv 15549 |
. . . . 5
β’ (π’ = π β Ξ£π β (1...4)((iβπ) Β· (((normCVβπ’)β(π₯( +π£ βπ’)((iβπ)( Β·π OLD
βπ’)π¦)))β2)) = Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2))) |
21 | 20 | oveq1d 7366 |
. . . 4
β’ (π’ = π β (Ξ£π β (1...4)((iβπ) Β· (((normCVβπ’)β(π₯( +π£ βπ’)((iβπ)( Β·π OLD
βπ’)π¦)))β2)) / 4) = (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4)) |
22 | 4, 4, 21 | mpoeq123dv 7426 |
. . 3
β’ (π’ = π β (π₯ β (BaseSetβπ’), π¦ β (BaseSetβπ’) β¦ (Ξ£π β (1...4)((iβπ) Β· (((normCVβπ’)β(π₯( +π£ βπ’)((iβπ)( Β·π OLD
βπ’)π¦)))β2)) / 4)) = (π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4))) |
23 | | df-dip 29472 |
. . 3
β’
Β·πOLD = (π’ β NrmCVec β¦ (π₯ β (BaseSetβπ’), π¦ β (BaseSetβπ’) β¦ (Ξ£π β (1...4)((iβπ) Β· (((normCVβπ’)β(π₯( +π£ βπ’)((iβπ)( Β·π OLD
βπ’)π¦)))β2)) / 4))) |
24 | 3 | fvexi 6853 |
. . . 4
β’ π β V |
25 | 24, 24 | mpoex 8004 |
. . 3
β’ (π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4)) β V |
26 | 22, 23, 25 | fvmpt 6945 |
. 2
β’ (π β NrmCVec β
(Β·πOLDβπ) = (π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4))) |
27 | 1, 26 | eqtrid 2789 |
1
β’ (π β NrmCVec β π = (π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4))) |