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

Definition df-lfig 30942
Description: Define the class of finitely generated left modules. Finite generation of subspaces can be intepreted using ↾s. (Contributed by Stefan O'Rear, 1-Jan-2015.)
Assertion
Ref Expression
df-lfig  |- LFinGen  =  {
w  e.  LMod  |  (
Base `  w )  e.  ( ( LSpan `  w
) " ( ~P ( Base `  w
)  i^i  Fin )
) }

Detailed syntax breakdown of Definition df-lfig
StepHypRef Expression
1 clfig 30941 . 2  class LFinGen
2 vw . . . . . 6  setvar  w
32cv 1378 . . . . 5  class  w
4 cbs 14507 . . . . 5  class  Base
53, 4cfv 5594 . . . 4  class  ( Base `  w )
6 clspn 17488 . . . . . 6  class  LSpan
73, 6cfv 5594 . . . . 5  class  ( LSpan `  w )
85cpw 4016 . . . . . 6  class  ~P ( Base `  w )
9 cfn 7528 . . . . . 6  class  Fin
108, 9cin 3480 . . . . 5  class  ( ~P ( Base `  w
)  i^i  Fin )
117, 10cima 5008 . . . 4  class  ( (
LSpan `  w ) "
( ~P ( Base `  w )  i^i  Fin ) )
125, 11wcel 1767 . . 3  wff  ( Base `  w )  e.  ( ( LSpan `  w ) " ( ~P ( Base `  w )  i^i 
Fin ) )
13 clmod 17383 . . 3  class  LMod
1412, 2, 13crab 2821 . 2  class  { w  e.  LMod  |  ( Base `  w )  e.  ( ( LSpan `  w ) " ( ~P ( Base `  w )  i^i 
Fin ) ) }
151, 14wceq 1379 1  wff LFinGen  =  {
w  e.  LMod  |  (
Base `  w )  e.  ( ( LSpan `  w
) " ( ~P ( Base `  w
)  i^i  Fin )
) }
Colors of variables: wff setvar class
This definition is referenced by:  islmodfg  30943  fglmod  30947
  Copyright terms: Public domain W3C validator