Definition df-nlm 24086

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 24080	. 2 class NrmMod
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1540	. . . . . 6 class 𝑓
4		cnrg 24079	. . . . . 6 class NrmRing
5	3, 4	wcel 2106	. . . . 5 wff 𝑓 ∈ NrmRing
6		vx	. . . . . . . . . . 11 setvar 𝑥
7	6	cv 1540	. . . . . . . . . 10 class 𝑥
8		vy	. . . . . . . . . . 11 setvar 𝑦
9	8	cv 1540	. . . . . . . . . 10 class 𝑦
10		vw	. . . . . . . . . . . 12 setvar 𝑤
11	10	cv 1540	. . . . . . . . . . 11 class 𝑤
12		cvsca 17197	. . . . . . . . . . 11 class ·𝑠
13	11, 12	cfv 6540	. . . . . . . . . 10 class ( ·𝑠 ‘𝑤)
14	7, 9, 13	co 7405	. . . . . . . . 9 class (𝑥( ·𝑠 ‘𝑤)𝑦)
15		cnm 24076	. . . . . . . . . 10 class norm
16	11, 15	cfv 6540	. . . . . . . . 9 class (norm‘𝑤)
17	14, 16	cfv 6540	. . . . . . . 8 class ((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦))
18	3, 15	cfv 6540	. . . . . . . . . 10 class (norm‘𝑓)
19	7, 18	cfv 6540	. . . . . . . . 9 class ((norm‘𝑓)‘𝑥)
20	9, 16	cfv 6540	. . . . . . . . 9 class ((norm‘𝑤)‘𝑦)
21		cmul 11111	. . . . . . . . 9 class ·
22	19, 20, 21	co 7405	. . . . . . . 8 class (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
23	17, 22	wceq 1541	. . . . . . 7 wff ((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
24		cbs 17140	. . . . . . . 8 class Base
25	11, 24	cfv 6540	. . . . . . 7 class (Base‘𝑤)
26	23, 8, 25	wral 3061	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
27	3, 24	cfv 6540	. . . . . 6 class (Base‘𝑓)
28	26, 6, 27	wral 3061	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
29	5, 28	wa 396	. . . 4 wff (𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))
30		csca 17196	. . . . 5 class Scalar
31	11, 30	cfv 6540	. . . 4 class (Scalar‘𝑤)
32	29, 2, 31	wsbc 3776	. . 3 wff [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))
33		cngp 24077	. . . 4 class NrmGrp
34		clmod 20463	. . . 4 class LMod
35	33, 34	cin 3946	. . 3 class (NrmGrp ∩ LMod)
36	32, 10, 35	crab 3432	. 2 class {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}
37	1, 36	wceq 1541	1 wff NrmMod = {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}

This definition is referenced by:  isnlm  24183