Definition df-nlm 22391

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 = { w e. (NrmGrp i^i LMod ) | [. (Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) }

Distinct variable group:   w, f, x, y

Detailed syntax breakdown of Definition df-nlm

Step	Hyp	Ref	Expression
1		cnlm 22385	. 2 class NrmMod
2		vf	. . . . . . 7 setvar f
3	2	cv 1482	. . . . . 6 class f
4		cnrg 22384	. . . . . 6 class NrmRing
5	3, 4	wcel 1990	. . . . 5 wff f e. NrmRing
6		vx	. . . . . . . . . . 11 setvar x
7	6	cv 1482	. . . . . . . . . 10 class x
8		vy	. . . . . . . . . . 11 setvar y
9	8	cv 1482	. . . . . . . . . 10 class y
10		vw	. . . . . . . . . . . 12 setvar w
11	10	cv 1482	. . . . . . . . . . 11 class w
12		cvsca 15945	. . . . . . . . . . 11 class .s
13	11, 12	cfv 5888	. . . . . . . . . 10 class ( .s ` w )
14	7, 9, 13	co 6650	. . . . . . . . 9 class ( x ( .s ` w ) y )
15		cnm 22381	. . . . . . . . . 10 class norm
16	11, 15	cfv 5888	. . . . . . . . 9 class ( norm ` w )
17	14, 16	cfv 5888	. . . . . . . 8 class ( ( norm ` w ) ` ( x ( .s ` w ) y ) )
18	3, 15	cfv 5888	. . . . . . . . . 10 class ( norm ` f )
19	7, 18	cfv 5888	. . . . . . . . 9 class ( ( norm ` f ) ` x )
20	9, 16	cfv 5888	. . . . . . . . 9 class ( ( norm ` w ) ` y )
21		cmul 9941	. . . . . . . . 9 class x.
22	19, 20, 21	co 6650	. . . . . . . 8 class ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) )
23	17, 22	wceq 1483	. . . . . . 7 wff ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) )
24		cbs 15857	. . . . . . . 8 class Base
25	11, 24	cfv 5888	. . . . . . 7 class ( Base ` w )
26	23, 8, 25	wral 2912	. . . . . 6 wff A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) )
27	3, 24	cfv 5888	. . . . . 6 class ( Base ` f )
28	26, 6, 27	wral 2912	. . . . 5 wff A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) )
29	5, 28	wa 384	. . . 4 wff ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) )
30		csca 15944	. . . . 5 class Scalar
31	11, 30	cfv 5888	. . . 4 class (Scalar ` w )
32	29, 2, 31	wsbc 3435	. . 3 wff [. (Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) )
33		cngp 22382	. . . 4 class NrmGrp
34		clmod 18863	. . . 4 class LMod
35	33, 34	cin 3573	. . 3 class (NrmGrp i^i LMod )
36	32, 10, 35	crab 2916	. 2 class { w e. (NrmGrp i^i LMod ) | [. (Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) }
37	1, 36	wceq 1483	1 wff NrmMod = { w e. (NrmGrp i^i LMod ) | [. (Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) }

This definition is referenced by:  isnlm  22479