Theorem islinindfiss

Description: The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-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	islinindfiss	|- ( ( M e. W /\ S e. Fin /\ S e. ~P B ) -> ( S linIndS M <-> A. f e. ( E ^m S ) ( ( 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	islinindfis	|- ( ( S e. Fin /\ M e. W ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) ) )
7	6	ancoms	|- ( ( M e. W /\ S e. Fin ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) ) )
8	7	3adant3	|- ( ( M e. W /\ S e. Fin /\ S e. ~P B ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) ) )
9	8	3anibar	|- ( ( M e. W /\ S e. Fin /\ S e. ~P B ) -> ( S linIndS M <-> A. f e. ( E ^m S ) ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) )