Description: The implications 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 | 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. ) ) ) |
| 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 | linindsv | |- ( S linIndS M -> ( S e. _V /\ M e. _V ) ) |
|
| 7 | 1 2 3 4 5 | islininds | |- ( ( S e. _V /\ M e. _V ) -> ( 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. ) ) ) ) |
| 8 | 6 7 | syl | |- ( S linIndS M -> ( 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. ) ) ) ) |
| 9 | 8 | ibi | |- ( 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. ) ) ) |