Step | Hyp | Ref
| Expression |
1 | | dipfval.1 |
. . . . 5
β’ π = (BaseSetβπ) |
2 | | dipfval.2 |
. . . . 5
β’ πΊ = ( +π£
βπ) |
3 | | dipfval.4 |
. . . . 5
β’ π = (
Β·π OLD βπ) |
4 | | dipfval.6 |
. . . . 5
β’ π =
(normCVβπ) |
5 | | dipfval.7 |
. . . . 5
β’ π =
(Β·πOLDβπ) |
6 | 1, 2, 3, 4, 5 | dipfval 29686 |
. . . 4
β’ (π β NrmCVec β π = (π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4))) |
7 | 6 | oveqd 7375 |
. . 3
β’ (π β NrmCVec β (π΄ππ΅) = (π΄(π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4))π΅)) |
8 | | fvoveq1 7381 |
. . . . . . . 8
β’ (π₯ = π΄ β (πβ(π₯πΊ((iβπ)ππ¦))) = (πβ(π΄πΊ((iβπ)ππ¦)))) |
9 | 8 | oveq1d 7373 |
. . . . . . 7
β’ (π₯ = π΄ β ((πβ(π₯πΊ((iβπ)ππ¦)))β2) = ((πβ(π΄πΊ((iβπ)ππ¦)))β2)) |
10 | 9 | oveq2d 7374 |
. . . . . 6
β’ (π₯ = π΄ β ((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) = ((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ¦)))β2))) |
11 | 10 | sumeq2sdv 15594 |
. . . . 5
β’ (π₯ = π΄ β Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) = Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ¦)))β2))) |
12 | 11 | oveq1d 7373 |
. . . 4
β’ (π₯ = π΄ β (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4) = (Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ¦)))β2)) / 4)) |
13 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π¦ = π΅ β ((iβπ)ππ¦) = ((iβπ)ππ΅)) |
14 | 13 | oveq2d 7374 |
. . . . . . . . 9
β’ (π¦ = π΅ β (π΄πΊ((iβπ)ππ¦)) = (π΄πΊ((iβπ)ππ΅))) |
15 | 14 | fveq2d 6847 |
. . . . . . . 8
β’ (π¦ = π΅ β (πβ(π΄πΊ((iβπ)ππ¦))) = (πβ(π΄πΊ((iβπ)ππ΅)))) |
16 | 15 | oveq1d 7373 |
. . . . . . 7
β’ (π¦ = π΅ β ((πβ(π΄πΊ((iβπ)ππ¦)))β2) = ((πβ(π΄πΊ((iβπ)ππ΅)))β2)) |
17 | 16 | oveq2d 7374 |
. . . . . 6
β’ (π¦ = π΅ β ((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ¦)))β2)) = ((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ΅)))β2))) |
18 | 17 | sumeq2sdv 15594 |
. . . . 5
β’ (π¦ = π΅ β Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ¦)))β2)) = Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ΅)))β2))) |
19 | 18 | oveq1d 7373 |
. . . 4
β’ (π¦ = π΅ β (Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ¦)))β2)) / 4) = (Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ΅)))β2)) / 4)) |
20 | | eqid 2733 |
. . . 4
β’ (π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4)) = (π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4)) |
21 | | ovex 7391 |
. . . 4
β’
(Ξ£π β
(1...4)((iβπ) Β·
((πβ(π΄πΊ((iβπ)ππ΅)))β2)) / 4) β V |
22 | 12, 19, 20, 21 | ovmpo 7516 |
. . 3
β’ ((π΄ β π β§ π΅ β π) β (π΄(π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4))π΅) = (Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ΅)))β2)) / 4)) |
23 | 7, 22 | sylan9eq 2793 |
. 2
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π)) β (π΄ππ΅) = (Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ΅)))β2)) / 4)) |
24 | 23 | 3impb 1116 |
1
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ΅)))β2)) / 4)) |