Theorem lindslinindimp2lem1

Description: Lemma 1 for lindslinindsimp2 . (Contributed by AV, 25-Apr-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	lindslinindimp2lem1	|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> Y e. B )

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	1	lmodfgrp	|- ( M e. LMod -> R e. Grp )
8	7	adantl	|- ( ( S e. V /\ M e. LMod ) -> R e. Grp )
9		elmapi	|- ( f e. ( B ^m S ) -> f : S --> B )
10		ffvelrn	|- ( ( f : S --> B /\ x e. S ) -> ( f ` x ) e. B )
11	10	a1d	|- ( ( f : S --> B /\ x e. S ) -> ( S C_ ( Base ` M ) -> ( f ` x ) e. B ) )
12	11	ex	|- ( f : S --> B -> ( x e. S -> ( S C_ ( Base ` M ) -> ( f ` x ) e. B ) ) )
13	9 12	syl	|- ( f e. ( B ^m S ) -> ( x e. S -> ( S C_ ( Base ` M ) -> ( f ` x ) e. B ) ) )
14	13	com13	|- ( S C_ ( Base ` M ) -> ( x e. S -> ( f e. ( B ^m S ) -> ( f ` x ) e. B ) ) )
15	14	3imp	|- ( ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) -> ( f ` x ) e. B )
16		eqid	|- ( invg ` R ) = ( invg ` R )
17	2 16	grpinvcl	|- ( ( R e. Grp /\ ( f ` x ) e. B ) -> ( ( invg ` R ) ` ( f ` x ) ) e. B )
18	8 15 17	syl2an	|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> ( ( invg ` R ) ` ( f ` x ) ) e. B )
19	5 18	eqeltrid	|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> Y e. B )