MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nlm Structured version   Visualization version   GIF version

Definition df-nlm 22438
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
StepHypRef Expression
1 cnlm 22432 . 2 class NrmMod
2 vf . . . . . . 7 setvar 𝑓
32cv 1522 . . . . . 6 class 𝑓
4 cnrg 22431 . . . . . 6 class NrmRing
53, 4wcel 2030 . . . . 5 wff 𝑓 ∈ NrmRing
6 vx . . . . . . . . . . 11 setvar 𝑥
76cv 1522 . . . . . . . . . 10 class 𝑥
8 vy . . . . . . . . . . 11 setvar 𝑦
98cv 1522 . . . . . . . . . 10 class 𝑦
10 vw . . . . . . . . . . . 12 setvar 𝑤
1110cv 1522 . . . . . . . . . . 11 class 𝑤
12 cvsca 15992 . . . . . . . . . . 11 class ·𝑠
1311, 12cfv 5926 . . . . . . . . . 10 class ( ·𝑠𝑤)
147, 9, 13co 6690 . . . . . . . . 9 class (𝑥( ·𝑠𝑤)𝑦)
15 cnm 22428 . . . . . . . . . 10 class norm
1611, 15cfv 5926 . . . . . . . . 9 class (norm‘𝑤)
1714, 16cfv 5926 . . . . . . . 8 class ((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦))
183, 15cfv 5926 . . . . . . . . . 10 class (norm‘𝑓)
197, 18cfv 5926 . . . . . . . . 9 class ((norm‘𝑓)‘𝑥)
209, 16cfv 5926 . . . . . . . . 9 class ((norm‘𝑤)‘𝑦)
21 cmul 9979 . . . . . . . . 9 class ·
2219, 20, 21co 6690 . . . . . . . 8 class (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
2317, 22wceq 1523 . . . . . . 7 wff ((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
24 cbs 15904 . . . . . . . 8 class Base
2511, 24cfv 5926 . . . . . . 7 class (Base‘𝑤)
2623, 8, 25wral 2941 . . . . . 6 wff 𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
273, 24cfv 5926 . . . . . 6 class (Base‘𝑓)
2826, 6, 27wral 2941 . . . . 5 wff 𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
295, 28wa 383 . . . 4 wff (𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))
30 csca 15991 . . . . 5 class Scalar
3111, 30cfv 5926 . . . 4 class (Scalar‘𝑤)
3229, 2, 31wsbc 3468 . . 3 wff [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))
33 cngp 22429 . . . 4 class NrmGrp
34 clmod 18911 . . . 4 class LMod
3533, 34cin 3606 . . 3 class (NrmGrp ∩ LMod)
3632, 10, 35crab 2945 . 2 class {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}
371, 36wceq 1523 1 wff NrmMod = {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}
Colors of variables: wff setvar class
This definition is referenced by:  isnlm  22526
  Copyright terms: Public domain W3C validator