Detailed syntax breakdown of Definition df-nlm
Step | Hyp | Ref
| Expression |
1 | | cnlm 23745 |
. 2
class
NrmMod |
2 | | vf |
. . . . . . 7
setvar 𝑓 |
3 | 2 | cv 1538 |
. . . . . 6
class 𝑓 |
4 | | cnrg 23744 |
. . . . . 6
class
NrmRing |
5 | 3, 4 | wcel 2107 |
. . . . 5
wff 𝑓 ∈ NrmRing |
6 | | vx |
. . . . . . . . . . 11
setvar 𝑥 |
7 | 6 | cv 1538 |
. . . . . . . . . 10
class 𝑥 |
8 | | vy |
. . . . . . . . . . 11
setvar 𝑦 |
9 | 8 | cv 1538 |
. . . . . . . . . 10
class 𝑦 |
10 | | vw |
. . . . . . . . . . . 12
setvar 𝑤 |
11 | 10 | cv 1538 |
. . . . . . . . . . 11
class 𝑤 |
12 | | cvsca 16975 |
. . . . . . . . . . 11
class
·𝑠 |
13 | 11, 12 | cfv 6437 |
. . . . . . . . . 10
class (
·𝑠 ‘𝑤) |
14 | 7, 9, 13 | co 7284 |
. . . . . . . . 9
class (𝑥(
·𝑠 ‘𝑤)𝑦) |
15 | | cnm 23741 |
. . . . . . . . . 10
class
norm |
16 | 11, 15 | cfv 6437 |
. . . . . . . . 9
class
(norm‘𝑤) |
17 | 14, 16 | cfv 6437 |
. . . . . . . 8
class
((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) |
18 | 3, 15 | cfv 6437 |
. . . . . . . . . 10
class
(norm‘𝑓) |
19 | 7, 18 | cfv 6437 |
. . . . . . . . 9
class
((norm‘𝑓)‘𝑥) |
20 | 9, 16 | cfv 6437 |
. . . . . . . . 9
class
((norm‘𝑤)‘𝑦) |
21 | | cmul 10885 |
. . . . . . . . 9
class
· |
22 | 19, 20, 21 | co 7284 |
. . . . . . . 8
class
(((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)) |
23 | 17, 22 | wceq 1539 |
. . . . . . 7
wff
((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)) |
24 | | cbs 16921 |
. . . . . . . 8
class
Base |
25 | 11, 24 | cfv 6437 |
. . . . . . 7
class
(Base‘𝑤) |
26 | 23, 8, 25 | wral 3065 |
. . . . . 6
wff
∀𝑦 ∈
(Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)) |
27 | 3, 24 | cfv 6437 |
. . . . . 6
class
(Base‘𝑓) |
28 | 26, 6, 27 | wral 3065 |
. . . . 5
wff
∀𝑥 ∈
(Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)) |
29 | 5, 28 | wa 396 |
. . . 4
wff (𝑓 ∈ NrmRing ∧
∀𝑥 ∈
(Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))) |
30 | | csca 16974 |
. . . . 5
class
Scalar |
31 | 11, 30 | cfv 6437 |
. . . 4
class
(Scalar‘𝑤) |
32 | 29, 2, 31 | wsbc 3717 |
. . 3
wff
[(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))) |
33 | | cngp 23742 |
. . . 4
class
NrmGrp |
34 | | clmod 20132 |
. . . 4
class
LMod |
35 | 33, 34 | cin 3887 |
. . 3
class (NrmGrp
∩ LMod) |
36 | 32, 10, 35 | crab 3069 |
. 2
class {𝑤 ∈ (NrmGrp ∩ LMod)
∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))} |
37 | 1, 36 | wceq 1539 |
1
wff NrmMod =
{𝑤 ∈ (NrmGrp ∩
LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠
‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))} |