Metamath Proof Explorer

Theorem linindscl

Description: A linearly independent set is a subset of (the base set of) a module. (Contributed by AV, 13-Apr-2019)

Ref Expression
Assertion linindscl 
|- ( S linIndS M -> S e. ~P ( Base ` M ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` M ) = ( Base ` M )
2 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
3 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
4 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
5 eqid 
 |-  ( 0g ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) )
6 1 2 3 4 5 linindsi 
 |-  ( 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 ) ) ) ) )
7 6 simpld 
 |-  ( S linIndS M -> S e. ~P ( Base ` M ) )