Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lnm Structured version   Visualization version   GIF version

Definition df-lnm 36460
Description: A left-module is Noetherian iff it is hereditarily finitely generated. (Contributed by Stefan O'Rear, 12-Dec-2014.)
Assertion
Ref Expression
df-lnm LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
Distinct variable group:   𝑤,𝑖

Detailed syntax breakdown of Definition df-lnm
StepHypRef Expression
1 clnm 36459 . 2 class LNoeM
2 vw . . . . . . 7 setvar 𝑤
32cv 1473 . . . . . 6 class 𝑤
4 vi . . . . . . 7 setvar 𝑖
54cv 1473 . . . . . 6 class 𝑖
6 cress 15642 . . . . . 6 class s
73, 5, 6co 6527 . . . . 5 class (𝑤s 𝑖)
8 clfig 36451 . . . . 5 class LFinGen
97, 8wcel 1976 . . . 4 wff (𝑤s 𝑖) ∈ LFinGen
10 clss 18699 . . . . 5 class LSubSp
113, 10cfv 5790 . . . 4 class (LSubSp‘𝑤)
129, 4, 11wral 2895 . . 3 wff 𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen
13 clmod 18632 . . 3 class LMod
1412, 2, 13crab 2899 . 2 class {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
151, 14wceq 1474 1 wff LNoeM = {𝑤 ∈ LMod ∣ ∀𝑖 ∈ (LSubSp‘𝑤)(𝑤s 𝑖) ∈ LFinGen}
Colors of variables: wff setvar class
This definition is referenced by:  islnm  36461
  Copyright terms: Public domain W3C validator