Metamath Proof Explorer

Theorem lincext2

Description: Property 2 of an extension of a linear combination. (Contributed by AV, 20-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses lincext.b 
|- B = ( Base ` M )
lincext.r 
|- R = ( Scalar ` M )
lincext.e 
|- E = ( Base ` R )
lincext.0 
|- .0. = ( 0g ` R )
lincext.z 
|- Z = ( 0g ` M )
lincext.n 
|- N = ( invg ` R )
lincext.f 
|- F = ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) )
Assertion lincext2 
|- ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> F finSupp .0. )

Proof

Step Hyp Ref Expression
1 lincext.b 
 |-  B = ( Base ` M )
2 lincext.r 
 |-  R = ( Scalar ` M )
3 lincext.e 
 |-  E = ( Base ` R )
4 lincext.0 
 |-  .0. = ( 0g ` R )
5 lincext.z 
 |-  Z = ( 0g ` M )
6 lincext.n 
 |-  N = ( invg ` R )
7 lincext.f 
 |-  F = ( z e. S |-> if ( z = X , ( N ` Y ) , ( G ` z ) ) )
8 fvex 
 |-  ( N ` Y ) e. _V
9 fvex 
 |-  ( G ` z ) e. _V
10 8 9 ifex 
 |-  if ( z = X , ( N ` Y ) , ( G ` z ) ) e. _V
11 10 7 dmmpti 
 |-  dom F = S
12 11 difeq1i 
 |-  ( dom F \ ( S \ { X } ) ) = ( S \ ( S \ { X } ) )
13 snssi 
 |-  ( X e. S -> { X } C_ S )
14 13 3ad2ant2 
 |-  ( ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) -> { X } C_ S )
15 14 3ad2ant2 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> { X } C_ S )
16 dfss4 
 |-  ( { X } C_ S <-> ( S \ ( S \ { X } ) ) = { X } )
17 15 16 sylib 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> ( S \ ( S \ { X } ) ) = { X } )
18 snfi 
 |-  { X } e. Fin
19 17 18 eqeltrdi 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> ( S \ ( S \ { X } ) ) e. Fin )
20 12 19 eqeltrid 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> ( dom F \ ( S \ { X } ) ) e. Fin )
21 1 2 3 4 5 6 7 lincext1 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> F e. ( E ^m S ) )
22 21 3adant3 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> F e. ( E ^m S ) )
23 elmapfun 
 |-  ( F e. ( E ^m S ) -> Fun F )
24 22 23 syl 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> Fun F )
25 elmapi 
 |-  ( G e. ( E ^m ( S \ { X } ) ) -> G : ( S \ { X } ) --> E )
26 7 fdmdifeqresdif 
 |-  ( G : ( S \ { X } ) --> E -> G = ( F |` ( S \ { X } ) ) )
27 25 26 syl 
 |-  ( G e. ( E ^m ( S \ { X } ) ) -> G = ( F |` ( S \ { X } ) ) )
28 27 3ad2ant3 
 |-  ( ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) -> G = ( F |` ( S \ { X } ) ) )
29 28 3ad2ant2 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> G = ( F |` ( S \ { X } ) ) )
30 simp3 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> G finSupp .0. )
31 4 fvexi 
 |-  .0. e. _V
32 31 a1i 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> .0. e. _V )
33 20 22 24 29 30 32 resfsupp 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ G finSupp .0. ) -> F finSupp .0. )