Metamath Proof Explorer

Theorem islininds

Description: The property of being a linearly independent subset. (Contributed by AV, 13-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses islininds.b 
|- B = ( Base ` M )
islininds.z 
|- Z = ( 0g ` M )
islininds.r 
|- R = ( Scalar ` M )
islininds.e 
|- E = ( Base ` R )
islininds.0 
|- .0. = ( 0g ` R )
Assertion islininds 
|- ( ( S e. V /\ M e. W ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) )

Proof

Step Hyp Ref Expression
1 islininds.b 
 |-  B = ( Base ` M )
2 islininds.z 
 |-  Z = ( 0g ` M )
3 islininds.r 
 |-  R = ( Scalar ` M )
4 islininds.e 
 |-  E = ( Base ` R )
5 islininds.0 
 |-  .0. = ( 0g ` R )
6 simpl 
 |-  ( ( s = S /\ m = M ) -> s = S )
7 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
8 7 1 eqtr4di 
 |-  ( m = M -> ( Base ` m ) = B )
9 8 adantl 
 |-  ( ( s = S /\ m = M ) -> ( Base ` m ) = B )
10 9 pweqd 
 |-  ( ( s = S /\ m = M ) -> ~P ( Base ` m ) = ~P B )
11 6 10 eleq12d 
 |-  ( ( s = S /\ m = M ) -> ( s e. ~P ( Base ` m ) <-> S e. ~P B ) )
12 fveq2 
 |-  ( m = M -> ( Scalar ` m ) = ( Scalar ` M ) )
13 12 3 eqtr4di 
 |-  ( m = M -> ( Scalar ` m ) = R )
14 13 fveq2d 
 |-  ( m = M -> ( Base ` ( Scalar ` m ) ) = ( Base ` R ) )
15 14 4 eqtr4di 
 |-  ( m = M -> ( Base ` ( Scalar ` m ) ) = E )
16 15 adantl 
 |-  ( ( s = S /\ m = M ) -> ( Base ` ( Scalar ` m ) ) = E )
17 16 6 oveq12d 
 |-  ( ( s = S /\ m = M ) -> ( ( Base ` ( Scalar ` m ) ) ^m s ) = ( E ^m S ) )
18 12 adantl 
 |-  ( ( s = S /\ m = M ) -> ( Scalar ` m ) = ( Scalar ` M ) )
19 18 3 eqtr4di 
 |-  ( ( s = S /\ m = M ) -> ( Scalar ` m ) = R )
20 19 fveq2d 
 |-  ( ( s = S /\ m = M ) -> ( 0g ` ( Scalar ` m ) ) = ( 0g ` R ) )
21 20 5 eqtr4di 
 |-  ( ( s = S /\ m = M ) -> ( 0g ` ( Scalar ` m ) ) = .0. )
22 21 breq2d 
 |-  ( ( s = S /\ m = M ) -> ( f finSupp ( 0g ` ( Scalar ` m ) ) <-> f finSupp .0. ) )
23 fveq2 
 |-  ( m = M -> ( linC ` m ) = ( linC ` M ) )
24 23 adantl 
 |-  ( ( s = S /\ m = M ) -> ( linC ` m ) = ( linC ` M ) )
25 eqidd 
 |-  ( ( s = S /\ m = M ) -> f = f )
26 24 25 6 oveq123d 
 |-  ( ( s = S /\ m = M ) -> ( f ( linC ` m ) s ) = ( f ( linC ` M ) S ) )
27 fveq2 
 |-  ( m = M -> ( 0g ` m ) = ( 0g ` M ) )
28 27 adantl 
 |-  ( ( s = S /\ m = M ) -> ( 0g ` m ) = ( 0g ` M ) )
29 28 2 eqtr4di 
 |-  ( ( s = S /\ m = M ) -> ( 0g ` m ) = Z )
30 26 29 eqeq12d 
 |-  ( ( s = S /\ m = M ) -> ( ( f ( linC ` m ) s ) = ( 0g ` m ) <-> ( f ( linC ` M ) S ) = Z ) )
31 22 30 anbi12d 
 |-  ( ( s = S /\ m = M ) -> ( ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) s ) = ( 0g ` m ) ) <-> ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) )
32 13 fveq2d 
 |-  ( m = M -> ( 0g ` ( Scalar ` m ) ) = ( 0g ` R ) )
33 32 5 eqtr4di 
 |-  ( m = M -> ( 0g ` ( Scalar ` m ) ) = .0. )
34 33 adantl 
 |-  ( ( s = S /\ m = M ) -> ( 0g ` ( Scalar ` m ) ) = .0. )
35 34 eqeq2d 
 |-  ( ( s = S /\ m = M ) -> ( ( f ` x ) = ( 0g ` ( Scalar ` m ) ) <-> ( f ` x ) = .0. ) )
36 6 35 raleqbidv 
 |-  ( ( s = S /\ m = M ) -> ( A. x e. s ( f ` x ) = ( 0g ` ( Scalar ` m ) ) <-> A. x e. S ( f ` x ) = .0. ) )
37 31 36 imbi12d 
 |-  ( ( s = S /\ m = M ) -> ( ( ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) s ) = ( 0g ` m ) ) -> A. x e. s ( f ` x ) = ( 0g ` ( Scalar ` m ) ) ) <-> ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
38 17 37 raleqbidv 
 |-  ( ( s = S /\ m = 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 ) ) ) <-> A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
39 11 38 anbi12d 
 |-  ( ( s = S /\ m = 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 ) ) ) ) <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) )
40 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 ) ) ) ) }
41 39 40 brabga 
 |-  ( ( S e. V /\ M e. W ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) )