Metamath Proof Explorer

Theorem lincext3

Description: Property 3 of an extension of a linear combination. (Contributed by AV, 23-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 lincext3 
|- ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> ( F ( linC ` M ) S ) = Z )

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 simp1l 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> M e. LMod )
9 simp1r 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> S e. ~P B )
10 simp2 
 |-  ( ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) -> X e. S )
11 10 3ad2ant2 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> X e. S )
12 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 ) )
13 12 3adant3 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> F e. ( E ^m S ) )
14 1 2 3 4 5 6 7 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. )
15 14 3adant3r 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> F finSupp .0. )
16 elmapi 
 |-  ( G e. ( E ^m ( S \ { X } ) ) -> G : ( S \ { X } ) --> E )
17 7 fdmdifeqresdif 
 |-  ( G : ( S \ { X } ) --> E -> G = ( F |` ( S \ { X } ) ) )
18 16 17 syl 
 |-  ( G e. ( E ^m ( S \ { X } ) ) -> G = ( F |` ( S \ { X } ) ) )
19 18 3ad2ant3 
 |-  ( ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) -> G = ( F |` ( S \ { X } ) ) )
20 19 3ad2ant2 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> G = ( F |` ( S \ { X } ) ) )
21 eqid 
 |-  ( .s ` M ) = ( .s ` M )
22 eqid 
 |-  ( +g ` M ) = ( +g ` M )
23 1 2 3 21 22 4 lincdifsn 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ X e. S ) /\ ( F e. ( E ^m S ) /\ F finSupp .0. ) /\ G = ( F |` ( S \ { X } ) ) ) -> ( F ( linC ` M ) S ) = ( ( G ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) )
24 8 9 11 13 15 20 23 syl321anc 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> ( F ( linC ` M ) S ) = ( ( G ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) )
25 oveq1 
 |-  ( ( G ( linC ` M ) ( S \ { X } ) ) = ( Y ( .s ` M ) X ) -> ( ( G ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) )
26 25 eqcoms 
 |-  ( ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) -> ( ( G ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) )
27 26 adantl 
 |-  ( ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) -> ( ( G ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) )
28 27 3ad2ant3 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> ( ( G ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) )
29 eqid 
 |-  ( invg ` M ) = ( invg ` M )
30 simpll 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> M e. LMod )
31 elelpwi 
 |-  ( ( X e. S /\ S e. ~P B ) -> X e. B )
32 31 expcom 
 |-  ( S e. ~P B -> ( X e. S -> X e. B ) )
33 32 adantl 
 |-  ( ( M e. LMod /\ S e. ~P B ) -> ( X e. S -> X e. B ) )
34 33 com12 
 |-  ( X e. S -> ( ( M e. LMod /\ S e. ~P B ) -> X e. B ) )
35 34 3ad2ant2 
 |-  ( ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) -> ( ( M e. LMod /\ S e. ~P B ) -> X e. B ) )
36 35 impcom 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> X e. B )
37 simpr1 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> Y e. E )
38 1 2 21 29 3 6 30 36 37 lmodvsneg 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( ( invg ` M ) ` ( Y ( .s ` M ) X ) ) = ( ( N ` Y ) ( .s ` M ) X ) )
39 iftrue 
 |-  ( z = X -> if ( z = X , ( N ` Y ) , ( G ` z ) ) = ( N ` Y ) )
40 10 adantl 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> X e. S )
41 fvexd 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( N ` Y ) e. _V )
42 7 39 40 41 fvmptd3 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( F ` X ) = ( N ` Y ) )
43 42 eqcomd 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( N ` Y ) = ( F ` X ) )
44 43 oveq1d 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( ( N ` Y ) ( .s ` M ) X ) = ( ( F ` X ) ( .s ` M ) X ) )
45 38 44 eqtr2d 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( ( F ` X ) ( .s ` M ) X ) = ( ( invg ` M ) ` ( Y ( .s ` M ) X ) ) )
46 45 oveq2d 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( invg ` M ) ` ( Y ( .s ` M ) X ) ) ) )
47 1 2 21 3 lmodvscl 
 |-  ( ( M e. LMod /\ Y e. E /\ X e. B ) -> ( Y ( .s ` M ) X ) e. B )
48 30 37 36 47 syl3anc 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( Y ( .s ` M ) X ) e. B )
49 1 22 5 29 lmodvnegid 
 |-  ( ( M e. LMod /\ ( Y ( .s ` M ) X ) e. B ) -> ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( invg ` M ) ` ( Y ( .s ` M ) X ) ) ) = Z )
50 30 48 49 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( invg ` M ) ` ( Y ( .s ` M ) X ) ) ) = Z )
51 46 50 eqtrd 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) ) -> ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z )
52 51 3adant3 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> ( ( Y ( .s ` M ) X ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z )
53 28 52 eqtrd 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> ( ( G ( linC ` M ) ( S \ { X } ) ) ( +g ` M ) ( ( F ` X ) ( .s ` M ) X ) ) = Z )
54 24 53 eqtrd 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( Y e. E /\ X e. S /\ G e. ( E ^m ( S \ { X } ) ) ) /\ ( G finSupp .0. /\ ( Y ( .s ` M ) X ) = ( G ( linC ` M ) ( S \ { X } ) ) ) ) -> ( F ( linC ` M ) S ) = Z )