Metamath Proof Explorer

Definition df-lininds

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)

Ref Expression
Assertion 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 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clininds 
 |-  linIndS
1 vs 
 |-  s
2 vm 
 |-  m
3 1 cv 
 |-  s
4 cbs 
 |-  Base
5 2 cv 
 |-  m
6 5 4 cfv 
 |-  ( Base ` m )
7 6 cpw 
 |-  ~P ( Base ` m )
8 3 7 wcel 
 |-  s e. ~P ( Base ` m )
9 vf 
 |-  f
10 csca 
 |-  Scalar
11 5 10 cfv 
 |-  ( Scalar ` m )
12 11 4 cfv 
 |-  ( Base ` ( Scalar ` m ) )
13 cmap 
 |-  ^m
14 12 3 13 co 
 |-  ( ( Base ` ( Scalar ` m ) ) ^m s )
15 9 cv 
 |-  f
16 cfsupp 
 |-  finSupp
17 c0g 
 |-  0g
18 11 17 cfv 
 |-  ( 0g ` ( Scalar ` m ) )
19 15 18 16 wbr 
 |-  f finSupp ( 0g ` ( Scalar ` m ) )
20 clinc 
 |-  linC
21 5 20 cfv 
 |-  ( linC ` m )
22 15 3 21 co 
 |-  ( f ( linC ` m ) s )
23 5 17 cfv 
 |-  ( 0g ` m )
24 22 23 wceq 
 |-  ( f ( linC ` m ) s ) = ( 0g ` m )
25 19 24 wa 
 |-  ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) s ) = ( 0g ` m ) )
26 vx 
 |-  x
27 26 cv 
 |-  x
28 27 15 cfv 
 |-  ( f ` x )
29 28 18 wceq 
 |-  ( f ` x ) = ( 0g ` ( Scalar ` m ) )
30 29 26 3 wral 
 |-  A. x e. s ( f ` x ) = ( 0g ` ( Scalar ` m ) )
31 25 30 wi 
 |-  ( ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) s ) = ( 0g ` m ) ) -> A. x e. s ( f ` x ) = ( 0g ` ( Scalar ` m ) ) )
32 31 9 14 wral 
 |-  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 ) ) )
33 8 32 wa 
 |-  ( 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 ) ) ) )
34 33 1 2 copab 
 |-  { <. 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 ) ) ) ) }
35 0 34 wceq 
 |-  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 ) ) ) ) }