Detailed syntax breakdown of Definition df-lno
Step | Hyp | Ref
| Expression |
1 | | clno 29096 |
. 2
class
LnOp |
2 | | vu |
. . 3
setvar 𝑢 |
3 | | vw |
. . 3
setvar 𝑤 |
4 | | cnv 28940 |
. . 3
class
NrmCVec |
5 | | vx |
. . . . . . . . . . . 12
setvar 𝑥 |
6 | 5 | cv 1541 |
. . . . . . . . . . 11
class 𝑥 |
7 | | vy |
. . . . . . . . . . . 12
setvar 𝑦 |
8 | 7 | cv 1541 |
. . . . . . . . . . 11
class 𝑦 |
9 | 2 | cv 1541 |
. . . . . . . . . . . 12
class 𝑢 |
10 | | cns 28943 |
. . . . . . . . . . . 12
class
·𝑠OLD |
11 | 9, 10 | cfv 6431 |
. . . . . . . . . . 11
class (
·𝑠OLD ‘𝑢) |
12 | 6, 8, 11 | co 7269 |
. . . . . . . . . 10
class (𝑥(
·𝑠OLD ‘𝑢)𝑦) |
13 | | vz |
. . . . . . . . . . 11
setvar 𝑧 |
14 | 13 | cv 1541 |
. . . . . . . . . 10
class 𝑧 |
15 | | cpv 28941 |
. . . . . . . . . . 11
class
+𝑣 |
16 | 9, 15 | cfv 6431 |
. . . . . . . . . 10
class (
+𝑣 ‘𝑢) |
17 | 12, 14, 16 | co 7269 |
. . . . . . . . 9
class ((𝑥(
·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧) |
18 | | vt |
. . . . . . . . . 10
setvar 𝑡 |
19 | 18 | cv 1541 |
. . . . . . . . 9
class 𝑡 |
20 | 17, 19 | cfv 6431 |
. . . . . . . 8
class (𝑡‘((𝑥( ·𝑠OLD
‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) |
21 | 8, 19 | cfv 6431 |
. . . . . . . . . 10
class (𝑡‘𝑦) |
22 | 3 | cv 1541 |
. . . . . . . . . . 11
class 𝑤 |
23 | 22, 10 | cfv 6431 |
. . . . . . . . . 10
class (
·𝑠OLD ‘𝑤) |
24 | 6, 21, 23 | co 7269 |
. . . . . . . . 9
class (𝑥(
·𝑠OLD ‘𝑤)(𝑡‘𝑦)) |
25 | 14, 19 | cfv 6431 |
. . . . . . . . 9
class (𝑡‘𝑧) |
26 | 22, 15 | cfv 6431 |
. . . . . . . . 9
class (
+𝑣 ‘𝑤) |
27 | 24, 25, 26 | co 7269 |
. . . . . . . 8
class ((𝑥(
·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) |
28 | 20, 27 | wceq 1542 |
. . . . . . 7
wff (𝑡‘((𝑥( ·𝑠OLD
‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) |
29 | | cba 28942 |
. . . . . . . 8
class
BaseSet |
30 | 9, 29 | cfv 6431 |
. . . . . . 7
class
(BaseSet‘𝑢) |
31 | 28, 13, 30 | wral 3066 |
. . . . . 6
wff
∀𝑧 ∈
(BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD
‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) |
32 | 31, 7, 30 | wral 3066 |
. . . . 5
wff
∀𝑦 ∈
(BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD
‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) |
33 | | cc 10868 |
. . . . 5
class
ℂ |
34 | 32, 5, 33 | wral 3066 |
. . . 4
wff
∀𝑥 ∈
ℂ ∀𝑦 ∈
(BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD
‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧)) |
35 | 22, 29 | cfv 6431 |
. . . . 5
class
(BaseSet‘𝑤) |
36 | | cmap 8596 |
. . . . 5
class
↑m |
37 | 35, 30, 36 | co 7269 |
. . . 4
class
((BaseSet‘𝑤)
↑m (BaseSet‘𝑢)) |
38 | 34, 18, 37 | crab 3070 |
. . 3
class {𝑡 ∈ ((BaseSet‘𝑤) ↑m
(BaseSet‘𝑢)) ∣
∀𝑥 ∈ ℂ
∀𝑦 ∈
(BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD
‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))} |
39 | 2, 3, 4, 4, 38 | cmpo 7271 |
. 2
class (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑m
(BaseSet‘𝑢)) ∣
∀𝑥 ∈ ℂ
∀𝑦 ∈
(BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD
‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))}) |
40 | 1, 39 | wceq 1542 |
1
wff LnOp =
(𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑m
(BaseSet‘𝑢)) ∣
∀𝑥 ∈ ℂ
∀𝑦 ∈
(BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD
‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD
‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))}) |