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 23332
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 23326 . 2 class NrmMod
2 vf . . . . . . 7 setvar 𝑓
32cv 1541 . . . . . 6 class 𝑓
4 cnrg 23325 . . . . . 6 class NrmRing
53, 4wcel 2113 . . . . 5 wff 𝑓 ∈ NrmRing
6 vx . . . . . . . . . . 11 setvar 𝑥
76cv 1541 . . . . . . . . . 10 class 𝑥
8 vy . . . . . . . . . . 11 setvar 𝑦
98cv 1541 . . . . . . . . . 10 class 𝑦
10 vw . . . . . . . . . . . 12 setvar 𝑤
1110cv 1541 . . . . . . . . . . 11 class 𝑤
12 cvsca 16665 . . . . . . . . . . 11 class ·𝑠
1311, 12cfv 6333 . . . . . . . . . 10 class ( ·𝑠𝑤)
147, 9, 13co 7164 . . . . . . . . 9 class (𝑥( ·𝑠𝑤)𝑦)
15 cnm 23322 . . . . . . . . . 10 class norm
1611, 15cfv 6333 . . . . . . . . 9 class (norm‘𝑤)
1714, 16cfv 6333 . . . . . . . 8 class ((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦))
183, 15cfv 6333 . . . . . . . . . 10 class (norm‘𝑓)
197, 18cfv 6333 . . . . . . . . 9 class ((norm‘𝑓)‘𝑥)
209, 16cfv 6333 . . . . . . . . 9 class ((norm‘𝑤)‘𝑦)
21 cmul 10613 . . . . . . . . 9 class ·
2219, 20, 21co 7164 . . . . . . . 8 class (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
2317, 22wceq 1542 . . . . . . 7 wff ((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
24 cbs 16579 . . . . . . . 8 class Base
2511, 24cfv 6333 . . . . . . 7 class (Base‘𝑤)
2623, 8, 25wral 3053 . . . . . 6 wff 𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
273, 24cfv 6333 . . . . . 6 class (Base‘𝑓)
2826, 6, 27wral 3053 . . . . 5 wff 𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦))
295, 28wa 399 . . . 4 wff (𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))
30 csca 16664 . . . . 5 class Scalar
3111, 30cfv 6333 . . . 4 class (Scalar‘𝑤)
3229, 2, 31wsbc 3679 . . 3 wff [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))
33 cngp 23323 . . . 4 class NrmGrp
34 clmod 19746 . . . 4 class LMod
3533, 34cin 3840 . . 3 class (NrmGrp ∩ LMod)
3632, 10, 35crab 3057 . 2 class {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}
371, 36wceq 1542 1 wff NrmMod = {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))}
Colors of variables: wff setvar class
This definition is referenced by:  isnlm  23421
  Copyright terms: Public domain W3C validator