Detailed syntax breakdown of Definition df-dip
| Step | Hyp | Ref
| Expression |
| 1 | | cdip 30719 |
. 2
class
·𝑖OLD |
| 2 | | vu |
. . 3
setvar 𝑢 |
| 3 | | cnv 30603 |
. . 3
class
NrmCVec |
| 4 | | vx |
. . . 4
setvar 𝑥 |
| 5 | | vy |
. . . 4
setvar 𝑦 |
| 6 | 2 | cv 1539 |
. . . . 5
class 𝑢 |
| 7 | | cba 30605 |
. . . . 5
class
BaseSet |
| 8 | 6, 7 | cfv 6561 |
. . . 4
class
(BaseSet‘𝑢) |
| 9 | | c1 11156 |
. . . . . . 7
class
1 |
| 10 | | c4 12323 |
. . . . . . 7
class
4 |
| 11 | | cfz 13547 |
. . . . . . 7
class
... |
| 12 | 9, 10, 11 | co 7431 |
. . . . . 6
class
(1...4) |
| 13 | | ci 11157 |
. . . . . . . 8
class
i |
| 14 | | vk |
. . . . . . . . 9
setvar 𝑘 |
| 15 | 14 | cv 1539 |
. . . . . . . 8
class 𝑘 |
| 16 | | cexp 14102 |
. . . . . . . 8
class
↑ |
| 17 | 13, 15, 16 | co 7431 |
. . . . . . 7
class
(i↑𝑘) |
| 18 | 4 | cv 1539 |
. . . . . . . . . 10
class 𝑥 |
| 19 | 5 | cv 1539 |
. . . . . . . . . . 11
class 𝑦 |
| 20 | | cns 30606 |
. . . . . . . . . . . 12
class
·𝑠OLD |
| 21 | 6, 20 | cfv 6561 |
. . . . . . . . . . 11
class (
·𝑠OLD ‘𝑢) |
| 22 | 17, 19, 21 | co 7431 |
. . . . . . . . . 10
class
((i↑𝑘)(
·𝑠OLD ‘𝑢)𝑦) |
| 23 | | cpv 30604 |
. . . . . . . . . . 11
class
+𝑣 |
| 24 | 6, 23 | cfv 6561 |
. . . . . . . . . 10
class (
+𝑣 ‘𝑢) |
| 25 | 18, 22, 24 | co 7431 |
. . . . . . . . 9
class (𝑥( +𝑣
‘𝑢)((i↑𝑘)(
·𝑠OLD ‘𝑢)𝑦)) |
| 26 | | cnmcv 30609 |
. . . . . . . . . 10
class
normCV |
| 27 | 6, 26 | cfv 6561 |
. . . . . . . . 9
class
(normCV‘𝑢) |
| 28 | 25, 27 | cfv 6561 |
. . . . . . . 8
class
((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦))) |
| 29 | | c2 12321 |
. . . . . . . 8
class
2 |
| 30 | 28, 29, 16 | co 7431 |
. . . . . . 7
class
(((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2) |
| 31 | | cmul 11160 |
. . . . . . 7
class
· |
| 32 | 17, 30, 31 | co 7431 |
. . . . . 6
class
((i↑𝑘) ·
(((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) |
| 33 | 12, 32, 14 | csu 15722 |
. . . . 5
class
Σ𝑘 ∈
(1...4)((i↑𝑘) ·
(((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) |
| 34 | | cdiv 11920 |
. . . . 5
class
/ |
| 35 | 33, 10, 34 | co 7431 |
. . . 4
class
(Σ𝑘 ∈
(1...4)((i↑𝑘) ·
(((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) / 4) |
| 36 | 4, 5, 8, 8, 35 | cmpo 7433 |
. . 3
class (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) / 4)) |
| 37 | 2, 3, 36 | cmpt 5225 |
. 2
class (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) / 4))) |
| 38 | 1, 37 | wceq 1540 |
1
wff
·𝑖OLD = (𝑢 ∈ NrmCVec ↦ (𝑥 ∈ (BaseSet‘𝑢), 𝑦 ∈ (BaseSet‘𝑢) ↦ (Σ𝑘 ∈ (1...4)((i↑𝑘) · (((normCV‘𝑢)‘(𝑥( +𝑣 ‘𝑢)((i↑𝑘)( ·𝑠OLD
‘𝑢)𝑦)))↑2)) / 4))) |