Metamath Proof Explorer

Theorem lindslinindimp2lem2

Description: Lemma 2 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 lindslinindimp2lem2 
|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> G e. ( B ^m ( S \ { x } ) ) )

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 elmapi 
 |-  ( f e. ( B ^m S ) -> f : S --> B )
8 7 3ad2ant3 
 |-  ( ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) -> f : S --> B )
9 8 adantl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> f : S --> B )
10 difss 
 |-  ( S \ { x } ) C_ S
11 fssres 
 |-  ( ( f : S --> B /\ ( S \ { x } ) C_ S ) -> ( f |` ( S \ { x } ) ) : ( S \ { x } ) --> B )
12 9 10 11 sylancl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> ( f |` ( S \ { x } ) ) : ( S \ { x } ) --> B )
13 6 feq1i 
 |-  ( G : ( S \ { x } ) --> B <-> ( f |` ( S \ { x } ) ) : ( S \ { x } ) --> B )
14 12 13 sylibr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> G : ( S \ { x } ) --> B )
15 2 fvexi 
 |-  B e. _V
16 difexg 
 |-  ( S e. V -> ( S \ { x } ) e. _V )
17 16 ad2antrr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> ( S \ { x } ) e. _V )
18 elmapg 
 |-  ( ( B e. _V /\ ( S \ { x } ) e. _V ) -> ( G e. ( B ^m ( S \ { x } ) ) <-> G : ( S \ { x } ) --> B ) )
19 15 17 18 sylancr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> ( G e. ( B ^m ( S \ { x } ) ) <-> G : ( S \ { x } ) --> B ) )
20 14 19 mpbird 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> G e. ( B ^m ( S \ { x } ) ) )