Metamath Proof Explorer

Theorem linindslinci

Description: The implications of being a linearly independent subset and a linear combination of this subset being 0. (Contributed by AV, 24-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 linindslinci 
|- ( ( S linIndS M /\ ( 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 1 2 3 4 5 linindsi 
 |-  ( 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. ) ) )
7 breq1 
 |-  ( f = F -> ( f finSupp .0. <-> F finSupp .0. ) )
8 oveq1 
 |-  ( f = F -> ( f ( linC ` M ) S ) = ( F ( linC ` M ) S ) )
9 8 eqeq1d 
 |-  ( f = F -> ( ( f ( linC ` M ) S ) = Z <-> ( F ( linC ` M ) S ) = Z ) )
10 7 9 anbi12d 
 |-  ( f = F -> ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) <-> ( F finSupp .0. /\ ( F ( linC ` M ) S ) = Z ) ) )
11 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
12 11 eqeq1d 
 |-  ( f = F -> ( ( f ` x ) = .0. <-> ( F ` x ) = .0. ) )
13 12 ralbidv 
 |-  ( f = F -> ( A. x e. S ( f ` x ) = .0. <-> A. x e. S ( F ` x ) = .0. ) )
14 10 13 imbi12d 
 |-  ( f = F -> ( ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> ( ( F finSupp .0. /\ ( F ( linC ` M ) S ) = Z ) -> A. x e. S ( F ` x ) = .0. ) ) )
15 14 rspcv 
 |-  ( F e. ( E ^m S ) -> ( A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( ( F finSupp .0. /\ ( F ( linC ` M ) S ) = Z ) -> A. x e. S ( F ` x ) = .0. ) ) )
16 15 com23 
 |-  ( F e. ( E ^m S ) -> ( ( F finSupp .0. /\ ( F ( linC ` M ) S ) = Z ) -> ( A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> A. x e. S ( F ` x ) = .0. ) ) )
17 16 3impib 
 |-  ( ( F e. ( E ^m S ) /\ F finSupp .0. /\ ( F ( linC ` M ) S ) = Z ) -> ( A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> A. x e. S ( F ` x ) = .0. ) )
18 17 com12 
 |-  ( A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( ( F e. ( E ^m S ) /\ F finSupp .0. /\ ( F ( linC ` M ) S ) = Z ) -> A. x e. S ( F ` x ) = .0. ) )
19 6 18 simpl2im 
 |-  ( S linIndS M -> ( ( F e. ( E ^m S ) /\ F finSupp .0. /\ ( F ( linC ` M ) S ) = Z ) -> A. x e. S ( F ` x ) = .0. ) )
20 19 imp 
 |-  ( ( S linIndS M /\ ( F e. ( E ^m S ) /\ F finSupp .0. /\ ( F ( linC ` M ) S ) = Z ) ) -> A. x e. S ( F ` x ) = .0. )