Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lininds Structured version   Unicode version

Definition df-lininds 31083
Description: Define the relation between a module and its linearly independent subsets. (Contributed by AV, 12-Apr-2019.) (Revised by AV, 24-Apr-2019.) (Revised by AV, 30-Jul-2019.)
Assertion
Ref Expression
df-lininds  |- linIndS  =  { <. s ,  m >.  |  ( s  e.  ~P ( Base `  m )  /\  A. f  e.  ( ( Base `  (Scalar `  m ) )  ^m  s ) ( ( f finSupp  ( 0g `  (Scalar `  m ) )  /\  ( f ( linC  `  m ) s )  =  ( 0g `  m ) )  ->  A. x  e.  s 
( f `  x
)  =  ( 0g
`  (Scalar `  m )
) ) ) }
Distinct variable group:    f, m, s, x

Detailed syntax breakdown of Definition df-lininds
StepHypRef Expression
1 clininds 31081 . 2  class linIndS
2 vs . . . . . 6  setvar  s
32cv 1369 . . . . 5  class  s
4 vm . . . . . . . 8  setvar  m
54cv 1369 . . . . . . 7  class  m
6 cbs 14276 . . . . . . 7  class  Base
75, 6cfv 5516 . . . . . 6  class  ( Base `  m )
87cpw 3958 . . . . 5  class  ~P ( Base `  m )
93, 8wcel 1758 . . . 4  wff  s  e. 
~P ( Base `  m
)
10 vf . . . . . . . . 9  setvar  f
1110cv 1369 . . . . . . . 8  class  f
12 csca 14343 . . . . . . . . . 10  class Scalar
135, 12cfv 5516 . . . . . . . . 9  class  (Scalar `  m )
14 c0g 14480 . . . . . . . . 9  class  0g
1513, 14cfv 5516 . . . . . . . 8  class  ( 0g
`  (Scalar `  m )
)
16 cfsupp 7721 . . . . . . . 8  class finSupp
1711, 15, 16wbr 4390 . . . . . . 7  wff  f finSupp  ( 0g `  (Scalar `  m
) )
18 clinc 31045 . . . . . . . . . 10  class linC
195, 18cfv 5516 . . . . . . . . 9  class  ( linC  `  m )
2011, 3, 19co 6190 . . . . . . . 8  class  ( f ( linC  `  m )
s )
215, 14cfv 5516 . . . . . . . 8  class  ( 0g
`  m )
2220, 21wceq 1370 . . . . . . 7  wff  ( f ( linC  `  m )
s )  =  ( 0g `  m )
2317, 22wa 369 . . . . . 6  wff  ( f finSupp 
( 0g `  (Scalar `  m ) )  /\  ( f ( linC  `  m ) s )  =  ( 0g `  m ) )
24 vx . . . . . . . . . 10  setvar  x
2524cv 1369 . . . . . . . . 9  class  x
2625, 11cfv 5516 . . . . . . . 8  class  ( f `
 x )
2726, 15wceq 1370 . . . . . . 7  wff  ( f `
 x )  =  ( 0g `  (Scalar `  m ) )
2827, 24, 3wral 2795 . . . . . 6  wff  A. x  e.  s  ( f `  x )  =  ( 0g `  (Scalar `  m ) )
2923, 28wi 4 . . . . 5  wff  ( ( f finSupp  ( 0g `  (Scalar `  m ) )  /\  ( f ( linC  `  m ) s )  =  ( 0g `  m ) )  ->  A. x  e.  s 
( f `  x
)  =  ( 0g
`  (Scalar `  m )
) )
3013, 6cfv 5516 . . . . . 6  class  ( Base `  (Scalar `  m )
)
31 cmap 7314 . . . . . 6  class  ^m
3230, 3, 31co 6190 . . . . 5  class  ( (
Base `  (Scalar `  m
) )  ^m  s
)
3329, 10, 32wral 2795 . . . 4  wff  A. f  e.  ( ( Base `  (Scalar `  m ) )  ^m  s ) ( ( f finSupp  ( 0g `  (Scalar `  m ) )  /\  ( f ( linC  `  m ) s )  =  ( 0g `  m ) )  ->  A. x  e.  s 
( f `  x
)  =  ( 0g
`  (Scalar `  m )
) )
349, 33wa 369 . . 3  wff  ( s  e.  ~P ( Base `  m )  /\  A. f  e.  ( ( Base `  (Scalar `  m
) )  ^m  s
) ( ( f finSupp 
( 0g `  (Scalar `  m ) )  /\  ( f ( linC  `  m ) s )  =  ( 0g `  m ) )  ->  A. x  e.  s 
( f `  x
)  =  ( 0g
`  (Scalar `  m )
) ) )
3534, 2, 4copab 4447 . 2  class  { <. s ,  m >.  |  ( s  e.  ~P ( Base `  m )  /\  A. f  e.  ( (
Base `  (Scalar `  m
) )  ^m  s
) ( ( f finSupp 
( 0g `  (Scalar `  m ) )  /\  ( f ( linC  `  m ) s )  =  ( 0g `  m ) )  ->  A. x  e.  s 
( f `  x
)  =  ( 0g
`  (Scalar `  m )
) ) ) }
361, 35wceq 1370 1  wff linIndS  =  { <. s ,  m >.  |  ( s  e.  ~P ( Base `  m )  /\  A. f  e.  ( ( Base `  (Scalar `  m ) )  ^m  s ) ( ( f finSupp  ( 0g `  (Scalar `  m ) )  /\  ( f ( linC  `  m ) s )  =  ( 0g `  m ) )  ->  A. x  e.  s 
( f `  x
)  =  ( 0g
`  (Scalar `  m )
) ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  rellininds  31084  islininds  31087
  Copyright terms: Public domain W3C validator