Theorem lindslinindimp2lem3

Description: Lemma 3 for lindslinindsimp2 . (Contributed by AV, 25-Apr-2019) (Revised by AV, 30-Jul-2019)

	Ref	Expression
Hypotheses	lindslinind.r	|- R = ( Scalar ` M )
	lindslinind.b	|- B = ( Base ` R )
	lindslinind.0	|- .0. = ( 0g ` R )
	lindslinind.z	|- Z = ( 0g ` M )
	lindslinind.y	|- Y = ( ( invg ` R ) ` ( f ` x ) )
	lindslinind.g	|- G = ( f |` ( S \ { x } ) )
Assertion	lindslinindimp2lem3	|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^m S ) /\ f finSupp .0. ) ) -> G finSupp .0. )

Proof

Step	Hyp	Ref	Expression
1		lindslinind.r	|- R = ( Scalar ` M )
2		lindslinind.b	|- B = ( Base ` R )
3		lindslinind.0	|- .0. = ( 0g ` R )
4		lindslinind.z	|- Z = ( 0g ` M )
5		lindslinind.y	|- Y = ( ( invg ` R ) ` ( f ` x ) )
6		lindslinind.g	|- G = ( f |` ( S \ { x } ) )
7		simp3r	|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^m S ) /\ f finSupp .0. ) ) -> f finSupp .0. )
8	3	fvexi	|- .0. e. _V
9	8	a1i	|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^m S ) /\ f finSupp .0. ) ) -> .0. e. _V )
10	7 9	fsuppres	|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^m S ) /\ f finSupp .0. ) ) -> ( f |` ( S \ { x } ) ) finSupp .0. )
11	6 10	eqbrtrid	|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^m S ) /\ f finSupp .0. ) ) -> G finSupp .0. )