Metamath Proof Explorer

Theorem lindslinindimp2lem4

Description: Lemma 4 for lindslinindsimp2 . (Contributed by AV, 25-Apr-2019) (Revised by AV, 30-Jul-2019) (Proof shortened by II, 16-Feb-2023)

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 lindslinindimp2lem4 
|- ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^m S ) /\ f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) 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 simpr 
 |-  ( ( S e. V /\ M e. LMod ) -> M e. LMod )
8 7 adantr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> M e. LMod )
9 simprl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> S C_ ( Base ` M ) )
10 elpwg 
 |-  ( S e. V -> ( S e. ~P ( Base ` M ) <-> S C_ ( Base ` M ) ) )
11 10 ad2antrr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( S e. ~P ( Base ` M ) <-> S C_ ( Base ` M ) ) )
12 9 11 mpbird 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> S e. ~P ( Base ` M ) )
13 simpr 
 |-  ( ( S C_ ( Base ` M ) /\ x e. S ) -> x e. S )
14 13 adantl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> x e. S )
15 8 12 14 3jca 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( M e. LMod /\ S e. ~P ( Base ` M ) /\ x e. S ) )
16 15 adantl 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( M e. LMod /\ S e. ~P ( Base ` M ) /\ x e. S ) )
17 simpl 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( f e. ( B ^m S ) /\ f finSupp .0. ) )
18 6 a1i 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> G = ( f |` ( S \ { x } ) ) )
19 eqid 
 |-  ( Base ` M ) = ( Base ` M )
20 eqid 
 |-  ( .s ` M ) = ( .s ` M )
21 eqid 
 |-  ( +g ` M ) = ( +g ` M )
22 19 1 2 20 21 3 lincdifsn 
 |-  ( ( ( M e. LMod /\ S e. ~P ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^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 ) ) )
23 16 17 18 22 syl3anc 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( f ( linC ` M ) S ) = ( ( G ( linC ` M ) ( S \ { x } ) ) ( +g ` M ) ( ( f ` x ) ( .s ` M ) x ) ) )
24 23 eqeq1d 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( f ( linC ` M ) S ) = Z <-> ( ( G ( linC ` M ) ( S \ { x } ) ) ( +g ` M ) ( ( f ` x ) ( .s ` M ) x ) ) = Z ) )
25 lmodgrp 
 |-  ( M e. LMod -> M e. Grp )
26 25 adantl 
 |-  ( ( S e. V /\ M e. LMod ) -> M e. Grp )
27 26 ad2antrl 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> M e. Grp )
28 7 ad2antrl 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> M e. LMod )
29 elmapi 
 |-  ( f e. ( B ^m S ) -> f : S --> B )
30 ffvelcdm 
 |-  ( ( f : S --> B /\ x e. S ) -> ( f ` x ) e. B )
31 30 expcom 
 |-  ( x e. S -> ( f : S --> B -> ( f ` x ) e. B ) )
32 31 ad2antll 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( f : S --> B -> ( f ` x ) e. B ) )
33 29 32 syl5com 
 |-  ( f e. ( B ^m S ) -> ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( f ` x ) e. B ) )
34 33 adantr 
 |-  ( ( f e. ( B ^m S ) /\ f finSupp .0. ) -> ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( f ` x ) e. B ) )
35 34 imp 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( f ` x ) e. B )
36 ssel2 
 |-  ( ( S C_ ( Base ` M ) /\ x e. S ) -> x e. ( Base ` M ) )
37 36 ad2antll 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> x e. ( Base ` M ) )
38 19 1 20 2 lmodvscl 
 |-  ( ( M e. LMod /\ ( f ` x ) e. B /\ x e. ( Base ` M ) ) -> ( ( f ` x ) ( .s ` M ) x ) e. ( Base ` M ) )
39 28 35 37 38 syl3anc 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( f ` x ) ( .s ` M ) x ) e. ( Base ` M ) )
40 difexg 
 |-  ( S e. V -> ( S \ { x } ) e. _V )
41 40 ad2antrr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( S \ { x } ) e. _V )
42 ssdifss 
 |-  ( S C_ ( Base ` M ) -> ( S \ { x } ) C_ ( Base ` M ) )
43 42 ad2antrl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( S \ { x } ) C_ ( Base ` M ) )
44 41 43 jca 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( ( S \ { x } ) e. _V /\ ( S \ { x } ) C_ ( Base ` M ) ) )
45 44 adantl 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( S \ { x } ) e. _V /\ ( S \ { x } ) C_ ( Base ` M ) ) )
46 simprl 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( S e. V /\ M e. LMod ) )
47 simpl 
 |-  ( ( S C_ ( Base ` M ) /\ x e. S ) -> S C_ ( Base ` M ) )
48 47 ad2antll 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> S C_ ( Base ` M ) )
49 13 ad2antll 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> x e. S )
50 simpl 
 |-  ( ( f e. ( B ^m S ) /\ f finSupp .0. ) -> f e. ( B ^m S ) )
51 50 adantr 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> f e. ( B ^m S ) )
52 1 2 3 4 5 6 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 } ) ) )
53 46 48 49 51 52 syl13anc 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> G e. ( B ^m ( S \ { x } ) ) )
54 simpr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( S C_ ( Base ` M ) /\ x e. S ) )
55 54 adantl 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( S C_ ( Base ` M ) /\ x e. S ) )
56 1 2 3 4 5 6 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. )
57 46 55 17 56 syl3anc 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> G finSupp .0. )
58 53 57 jca 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( G e. ( B ^m ( S \ { x } ) ) /\ G finSupp .0. ) )
59 19 1 2 3 lincfsuppcl 
 |-  ( ( M e. LMod /\ ( ( S \ { x } ) e. _V /\ ( S \ { x } ) C_ ( Base ` M ) ) /\ ( G e. ( B ^m ( S \ { x } ) ) /\ G finSupp .0. ) ) -> ( G ( linC ` M ) ( S \ { x } ) ) e. ( Base ` M ) )
60 28 45 58 59 syl3anc 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( G ( linC ` M ) ( S \ { x } ) ) e. ( Base ` M ) )
61 eqid 
 |-  ( invg ` M ) = ( invg ` M )
62 19 21 4 61 grpinvid2 
 |-  ( ( M e. Grp /\ ( ( f ` x ) ( .s ` M ) x ) e. ( Base ` M ) /\ ( G ( linC ` M ) ( S \ { x } ) ) e. ( Base ` M ) ) -> ( ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) = ( G ( linC ` M ) ( S \ { x } ) ) <-> ( ( G ( linC ` M ) ( S \ { x } ) ) ( +g ` M ) ( ( f ` x ) ( .s ` M ) x ) ) = Z ) )
63 27 39 60 62 syl3anc 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) = ( G ( linC ` M ) ( S \ { x } ) ) <-> ( ( G ( linC ` M ) ( S \ { x } ) ) ( +g ` M ) ( ( f ` x ) ( .s ` M ) x ) ) = Z ) )
64 24 63 bitr4d 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( f ( linC ` M ) S ) = Z <-> ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) = ( G ( linC ` M ) ( S \ { x } ) ) ) )
65 eqcom 
 |-  ( ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) = ( G ( linC ` M ) ( S \ { x } ) ) <-> ( G ( linC ` M ) ( S \ { x } ) ) = ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) )
66 1 fveq2i 
 |-  ( Base ` R ) = ( Base ` ( Scalar ` M ) )
67 2 66 eqtri 
 |-  B = ( Base ` ( Scalar ` M ) )
68 67 oveq1i 
 |-  ( B ^m ( S \ { x } ) ) = ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { x } ) )
69 53 68 eleqtrdi 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> G e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { x } ) ) )
70 41 43 elpwd 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( S \ { x } ) e. ~P ( Base ` M ) )
71 70 adantl 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( S \ { x } ) e. ~P ( Base ` M ) )
72 lincval 
 |-  ( ( M e. LMod /\ G e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { x } ) ) /\ ( S \ { x } ) e. ~P ( Base ` M ) ) -> ( G ( linC ` M ) ( S \ { x } ) ) = ( M gsum ( y e. ( S \ { x } ) |-> ( ( G ` y ) ( .s ` M ) y ) ) ) )
73 28 69 71 72 syl3anc 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( G ( linC ` M ) ( S \ { x } ) ) = ( M gsum ( y e. ( S \ { x } ) |-> ( ( G ` y ) ( .s ` M ) y ) ) ) )
74 73 eqeq1d 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( G ( linC ` M ) ( S \ { x } ) ) = ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) <-> ( M gsum ( y e. ( S \ { x } ) |-> ( ( G ` y ) ( .s ` M ) y ) ) ) = ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) ) )
75 6 fveq1i 
 |-  ( G ` y ) = ( ( f |` ( S \ { x } ) ) ` y )
76 75 a1i 
 |-  ( ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) /\ y e. ( S \ { x } ) ) -> ( G ` y ) = ( ( f |` ( S \ { x } ) ) ` y ) )
77 fvres 
 |-  ( y e. ( S \ { x } ) -> ( ( f |` ( S \ { x } ) ) ` y ) = ( f ` y ) )
78 77 adantl 
 |-  ( ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) /\ y e. ( S \ { x } ) ) -> ( ( f |` ( S \ { x } ) ) ` y ) = ( f ` y ) )
79 76 78 eqtrd 
 |-  ( ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) /\ y e. ( S \ { x } ) ) -> ( G ` y ) = ( f ` y ) )
80 79 oveq1d 
 |-  ( ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) /\ y e. ( S \ { x } ) ) -> ( ( G ` y ) ( .s ` M ) y ) = ( ( f ` y ) ( .s ` M ) y ) )
81 80 mpteq2dva 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( y e. ( S \ { x } ) |-> ( ( G ` y ) ( .s ` M ) y ) ) = ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) )
82 81 oveq2d 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( G ` y ) ( .s ` M ) y ) ) ) = ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) )
83 eqid 
 |-  ( invg ` R ) = ( invg ` R )
84 19 1 20 61 2 83 28 37 35 lmodvsneg 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) = ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) )
85 5 eqcomi 
 |-  ( ( invg ` R ) ` ( f ` x ) ) = Y
86 85 a1i 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( invg ` R ) ` ( f ` x ) ) = Y )
87 86 oveq1d 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( Y ( .s ` M ) x ) )
88 84 87 eqtrd 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) = ( Y ( .s ` M ) x ) )
89 82 88 eqeq12d 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( M gsum ( y e. ( S \ { x } ) |-> ( ( G ` y ) ( .s ` M ) y ) ) ) = ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) <-> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) ) )
90 89 biimpd 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( M gsum ( y e. ( S \ { x } ) |-> ( ( G ` y ) ( .s ` M ) y ) ) ) = ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) ) )
91 74 90 sylbid 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( G ( linC ` M ) ( S \ { x } ) ) = ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) ) )
92 65 91 biimtrid 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( ( invg ` M ) ` ( ( f ` x ) ( .s ` M ) x ) ) = ( G ( linC ` M ) ( S \ { x } ) ) -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) ) )
93 64 92 sylbid 
 |-  ( ( ( f e. ( B ^m S ) /\ f finSupp .0. ) /\ ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) ) -> ( ( f ( linC ` M ) S ) = Z -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) ) )
94 93 ex 
 |-  ( ( f e. ( B ^m S ) /\ f finSupp .0. ) -> ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( ( f ( linC ` M ) S ) = Z -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) ) ) )
95 94 com23 
 |-  ( ( f e. ( B ^m S ) /\ f finSupp .0. ) -> ( ( f ( linC ` M ) S ) = Z -> ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) ) ) )
96 95 3impia 
 |-  ( ( f e. ( B ^m S ) /\ f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) ) )
97 96 com12 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( ( f e. ( B ^m S ) /\ f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) ) )
98 97 3impia 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) /\ ( f e. ( B ^m S ) /\ f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( M gsum ( y e. ( S \ { x } ) |-> ( ( f ` y ) ( .s ` M ) y ) ) ) = ( Y ( .s ` M ) x ) )