Metamath Proof Explorer

Theorem lindslininds

Description: Equivalence of definitions df-linds and df-lininds for (linear) independence for (left) modules. (Contributed by AV, 26-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion lindslininds 
|- ( ( S e. V /\ M e. LMod ) -> ( S linIndS M <-> S e. ( LIndS ` M ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
2 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
3 eqid 
 |-  ( 0g ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) )
4 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
5 1 2 3 4 lindslinindsimp1 
 |-  ( ( S e. V /\ M e. LMod ) -> ( ( 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 C_ ( Base ` M ) /\ A. s e. S A. g e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) -. ( g ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) )
6 1 2 3 4 lindslinindsimp2 
 |-  ( ( S e. V /\ M e. LMod ) -> ( ( S C_ ( Base ` M ) /\ A. s e. S A. g e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) -. ( g ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) -> ( 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 ) ) ) ) ) )
7 5 6 impbid 
 |-  ( ( S e. V /\ M e. LMod ) -> ( ( 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 C_ ( Base ` M ) /\ A. s e. S A. g e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) -. ( g ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) )
8 eqid 
 |-  ( Base ` M ) = ( Base ` M )
9 8 4 1 2 3 islininds 
 |-  ( ( S e. V /\ M e. LMod ) -> ( S linIndS 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 ) ) ) ) ) )
10 eqid 
 |-  ( .s ` M ) = ( .s ` M )
11 eqid 
 |-  ( LSpan ` M ) = ( LSpan ` M )
12 8 10 11 1 2 3 islinds2 
 |-  ( M e. LMod -> ( S e. ( LIndS ` M ) <-> ( S C_ ( Base ` M ) /\ A. s e. S A. g e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) -. ( g ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) )
13 12 adantl 
 |-  ( ( S e. V /\ M e. LMod ) -> ( S e. ( LIndS ` M ) <-> ( S C_ ( Base ` M ) /\ A. s e. S A. g e. ( ( Base ` ( Scalar ` M ) ) \ { ( 0g ` ( Scalar ` M ) ) } ) -. ( g ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) )
14 7 9 13 3bitr4d 
 |-  ( ( S e. V /\ M e. LMod ) -> ( S linIndS M <-> S e. ( LIndS ` M ) ) )