df-nlm

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)

		Ref	Expression
	Assertion	df-nlm	$⊢ NrmMod = \{w \in (NrmGrp \cap LMod) \| \underset{˙}{[} Scalar (w) / f \underset{˙}{]} (f \in NrmRing \land \forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnlm	$class NrmMod$
1		vw	$setvar w$
2		cngp	$class NrmGrp$
3		clmod	$class LMod$
4	2 3	cin	$class (NrmGrp \cap LMod)$
5		csca	$class Scalar$
6	1	cv	$setvar w$
7	6 5	cfv	$class Scalar (w)$
8		vf	$setvar f$
9	8	cv	$setvar f$
10		cnrg	$class NrmRing$
11	9 10	wcel	$wff f \in NrmRing$
12		vx	$setvar x$
13		cbs	$class Base$
14	9 13	cfv	$class {Base}_{f}$
15		vy	$setvar y$
16	6 13	cfv	$class {Base}_{w}$
17		cnm	$class norm$
18	6 17	cfv	$class norm (w)$
19	12	cv	$setvar x$
20		cvsca	$class \cdot_{𝑠}$
21	6 20	cfv	$class \cdot_{w}$
22	15	cv	$setvar y$
23	19 22 21	co	$class (x \cdot_{w} y)$
24	23 18	cfv	$class norm (w) (x \cdot_{w} y)$
25	9 17	cfv	$class norm (f)$
26	19 25	cfv	$class norm (f) (x)$
27		cmul	$class \times$
28	22 18	cfv	$class norm (w) (y)$
29	26 28 27	co	$class norm (f) (x) norm (w) (y)$
30	24 29	wceq	$wff norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y)$
31	30 15 16	wral	$wff \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y)$
32	31 12 14	wral	$wff \forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y)$
33	11 32	wa	$wff (f \in NrmRing \land \forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y))$
34	33 8 7	wsbc	$wff \underset{˙}{[} Scalar (w) / f \underset{˙}{]} (f \in NrmRing \land \forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y))$
35	34 1 4	crab	$class \{w \in (NrmGrp \cap LMod) \| \underset{˙}{[} Scalar (w) / f \underset{˙}{]} (f \in NrmRing \land \forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y))\}$
36	0 35	wceq	$wff NrmMod = \{w \in (NrmGrp \cap LMod) \| \underset{˙}{[} Scalar (w) / f \underset{˙}{]} (f \in NrmRing \land \forall x \in {Base}_{f} \forall y \in {Base}_{w} norm (w) (x \cdot_{w} y) = norm (f) (x) norm (w) (y))\}$

Metamath Proof Explorer

Definition df-nlm

Detailed syntax breakdown