Metamath Proof Explorer

Definition 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 ∈ NrmGrp ∩ LMod | [˙ Scalar ⁡ w / f]˙ f ∈ NrmRing ∧ ∀ x ∈ Base f ∀ y ∈ Base w norm ⁡ w ⁡ x ⋅ 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 ∩ 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 ∈ 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 ⋅ 𝑠
21 6 20 cfv class ⋅ w
22 15 cv setvar y
23 19 22 21 co class x ⋅ w y
24 23 18 cfv class norm ⁡ w ⁡ x ⋅ w y
25 9 17 cfv class norm ⁡ f
26 19 25 cfv class norm ⁡ f ⁡ x
27 cmul class ×
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 ⋅ w y = norm ⁡ f ⁡ x ⁢ norm ⁡ w ⁡ y
31 30 15 16 wral wff ∀ y ∈ Base w norm ⁡ w ⁡ x ⋅ w y = norm ⁡ f ⁡ x ⁢ norm ⁡ w ⁡ y
32 31 12 14 wral wff ∀ x ∈ Base f ∀ y ∈ Base w norm ⁡ w ⁡ x ⋅ w y = norm ⁡ f ⁡ x ⁢ norm ⁡ w ⁡ y
33 11 32 wa wff f ∈ NrmRing ∧ ∀ x ∈ Base f ∀ y ∈ Base w norm ⁡ w ⁡ x ⋅ w y = norm ⁡ f ⁡ x ⁢ norm ⁡ w ⁡ y
34 33 8 7 wsbc wff [˙ Scalar ⁡ w / f]˙ f ∈ NrmRing ∧ ∀ x ∈ Base f ∀ y ∈ Base w norm ⁡ w ⁡ x ⋅ w y = norm ⁡ f ⁡ x ⁢ norm ⁡ w ⁡ y
35 34 1 4 crab class w ∈ NrmGrp ∩ LMod | [˙ Scalar ⁡ w / f]˙ f ∈ NrmRing ∧ ∀ x ∈ Base f ∀ y ∈ Base w norm ⁡ w ⁡ x ⋅ w y = norm ⁡ f ⁡ x ⁢ norm ⁡ w ⁡ y
36 0 35 wceq wff NrmMod = w ∈ NrmGrp ∩ LMod | [˙ Scalar ⁡ w / f]˙ f ∈ NrmRing ∧ ∀ x ∈ Base f ∀ y ∈ Base w norm ⁡ w ⁡ x ⋅ w y = norm ⁡ f ⁡ x ⁢ norm ⁡ w ⁡ y