Definition df-nlm 24599

Description: A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015.)

Assertion

Ref	Expression
df-nlm	⊢ NrmMod = {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}

Distinct variable group:   𝑤,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-nlm

Step	Hyp	Ref	Expression
1		cnlm 24593	. 2 class NrmMod
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1539	. . . . . 6 class 𝑓
4		cnrg 24592	. . . . . 6 class NrmRing
5	3, 4	wcel 2108	. . . . 5 wff 𝑓 ∈ NrmRing
6		vx	. . . . . . . . . . 11 setvar 𝑥
7	6	cv 1539	. . . . . . . . . 10 class 𝑥
8		vy	. . . . . . . . . . 11 setvar 𝑦
9	8	cv 1539	. . . . . . . . . 10 class 𝑦
10		vw	. . . . . . . . . . . 12 setvar 𝑤
11	10	cv 1539	. . . . . . . . . . 11 class 𝑤
12		cvsca 17301	. . . . . . . . . . 11 class ·𝑠
13	11, 12	cfv 6561	. . . . . . . . . 10 class ( ·𝑠 ‘𝑤)
14	7, 9, 13	co 7431	. . . . . . . . 9 class (𝑥( ·𝑠 ‘𝑤)𝑦)
15		cnm 24589	. . . . . . . . . 10 class norm
16	11, 15	cfv 6561	. . . . . . . . 9 class (norm‘𝑤)
17	14, 16	cfv 6561	. . . . . . . 8 class ((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦))
18	3, 15	cfv 6561	. . . . . . . . . 10 class (norm‘𝑓)
19	7, 18	cfv 6561	. . . . . . . . 9 class ((norm‘𝑓)‘𝑥)
20	9, 16	cfv 6561	. . . . . . . . 9 class ((norm‘𝑤)‘𝑦)
21		cmul 11160	. . . . . . . . 9 class ·
22	19, 20, 21	co 7431	. . . . . . . 8 class (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
23	17, 22	wceq 1540	. . . . . . 7 wff ((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
24		cbs 17247	. . . . . . . 8 class Base
25	11, 24	cfv 6561	. . . . . . 7 class (Base‘𝑤)
26	23, 8, 25	wral 3061	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
27	3, 24	cfv 6561	. . . . . 6 class (Base‘𝑓)
28	26, 6, 27	wral 3061	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
29	5, 28	wa 395	. . . 4 wff (𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))
30		csca 17300	. . . . 5 class Scalar
31	11, 30	cfv 6561	. . . 4 class (Scalar‘𝑤)
32	29, 2, 31	wsbc 3788	. . 3 wff [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))
33		cngp 24590	. . . 4 class NrmGrp
34		clmod 20858	. . . 4 class LMod
35	33, 34	cin 3950	. . 3 class (NrmGrp ∩ LMod)
36	32, 10, 35	crab 3436	. 2 class {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}
37	1, 36	wceq 1540	1 wff NrmMod = {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}

This definition is referenced by:  isnlm  24696