Metamath Proof Explorer

Theorem lindslinindsimp2lem5

Description: Lemma 5 for lindslinindsimp2 . (Contributed by AV, 25-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses lindslinind.r 
|- R = ( Scalar ` M )
lindslinind.b 
|- B = ( Base ` R )
lindslinind.0 
|- .0. = ( 0g ` R )
lindslinind.z 
|- Z = ( 0g ` M )
Assertion lindslinindsimp2lem5 
|- ( ( ( 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 ) ) -> ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) ) )

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 ax-1 
 |-  ( ( f ` x ) = .0. -> ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) )
6 5 2a1d 
 |-  ( ( f ` x ) = .0. -> ( ( ( 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 ) ) -> ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) ) ) )
7 elmapi 
 |-  ( f e. ( B ^m S ) -> f : S --> B )
8 ffvelrn 
 |-  ( ( f : S --> B /\ x e. S ) -> ( f ` x ) e. B )
9 8 expcom 
 |-  ( x e. S -> ( f : S --> B -> ( f ` x ) e. B ) )
10 9 adantl 
 |-  ( ( S C_ ( Base ` M ) /\ x e. S ) -> ( f : S --> B -> ( f ` x ) e. B ) )
11 10 adantl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( f : S --> B -> ( f ` x ) e. B ) )
12 11 com12 
 |-  ( f : S --> B -> ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( f ` x ) e. B ) )
13 7 12 syl 
 |-  ( f e. ( B ^m S ) -> ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( f ` x ) e. B ) )
14 13 adantr 
 |-  ( ( 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 ) ) -> ( f ` x ) e. B ) )
15 14 impcom 
 |-  ( ( ( ( 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 ) ) ) -> ( f ` x ) e. B )
16 15 biantrurd 
 |-  ( ( ( ( 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 ) ) ) -> ( ( f ` x ) =/= .0. <-> ( ( f ` x ) e. B /\ ( f ` x ) =/= .0. ) ) )
17 df-ne 
 |-  ( ( f ` x ) =/= .0. <-> -. ( f ` x ) = .0. )
18 17 bicomi 
 |-  ( -. ( f ` x ) = .0. <-> ( f ` x ) =/= .0. )
19 eldifsn 
 |-  ( ( f ` x ) e. ( B \ { .0. } ) <-> ( ( f ` x ) e. B /\ ( f ` x ) =/= .0. ) )
20 16 18 19 3bitr4g 
 |-  ( ( ( ( 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 ) ) ) -> ( -. ( f ` x ) = .0. <-> ( f ` x ) e. ( B \ { .0. } ) ) )
21 1 lmodfgrp 
 |-  ( M e. LMod -> R e. Grp )
22 21 adantl 
 |-  ( ( S e. V /\ M e. LMod ) -> R e. Grp )
23 22 adantr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> R e. Grp )
24 23 adantr 
 |-  ( ( ( ( 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 ) ) ) -> R e. Grp )
25 eqid 
 |-  ( invg ` R ) = ( invg ` R )
26 2 3 25 grpinvnzcl 
 |-  ( ( R e. Grp /\ ( f ` x ) e. ( B \ { .0. } ) ) -> ( ( invg ` R ) ` ( f ` x ) ) e. ( B \ { .0. } ) )
27 24 26 sylan 
 |-  ( ( ( ( ( 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 ) ) ) /\ ( f ` x ) e. ( B \ { .0. } ) ) -> ( ( invg ` R ) ` ( f ` x ) ) e. ( B \ { .0. } ) )
28 27 ex 
 |-  ( ( ( ( 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 ) ) ) -> ( ( f ` x ) e. ( B \ { .0. } ) -> ( ( invg ` R ) ` ( f ` x ) ) e. ( B \ { .0. } ) ) )
29 20 28 sylbid 
 |-  ( ( ( ( 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 ) ) ) -> ( -. ( f ` x ) = .0. -> ( ( invg ` R ) ` ( f ` x ) ) e. ( B \ { .0. } ) ) )
30 oveq1 
 |-  ( y = ( ( invg ` R ) ` ( f ` x ) ) -> ( y ( .s ` M ) x ) = ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) )
31 30 eqeq1d 
 |-  ( y = ( ( invg ` R ) ` ( f ` x ) ) -> ( ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) <-> ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) )
32 31 notbid 
 |-  ( y = ( ( invg ` R ) ` ( f ` x ) ) -> ( -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) <-> -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) )
33 32 orbi2d 
 |-  ( y = ( ( invg ` R ) ` ( f ` x ) ) -> ( ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) <-> ( -. g finSupp .0. \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) ) )
34 33 ralbidv 
 |-  ( y = ( ( invg ` R ) ` ( f ` x ) ) -> ( A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) <-> A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) ) )
35 34 rspcva 
 |-  ( ( ( ( invg ` R ) ` ( f ` x ) ) e. ( B \ { .0. } ) /\ A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) ) -> A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) )
36 simpl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( S e. V /\ M e. LMod ) )
37 36 adantr 
 |-  ( ( ( ( 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 ) ) ) -> ( S e. V /\ M e. LMod ) )
38 simplrl 
 |-  ( ( ( ( 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 ) ) ) -> S C_ ( Base ` M ) )
39 simplrr 
 |-  ( ( ( ( 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 ) ) ) -> x e. S )
40 simpl 
 |-  ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> f e. ( B ^m S ) )
41 40 adantl 
 |-  ( ( ( ( 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 ) ) ) -> f e. ( B ^m S ) )
42 eqid 
 |-  ( ( invg ` R ) ` ( f ` x ) ) = ( ( invg ` R ) ` ( f ` x ) )
43 eqid 
 |-  ( f |` ( S \ { x } ) ) = ( f |` ( S \ { x } ) )
44 1 2 3 4 42 43 lindslinindimp2lem2 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S /\ f e. ( B ^m S ) ) ) -> ( f |` ( S \ { x } ) ) e. ( B ^m ( S \ { x } ) ) )
45 37 38 39 41 44 syl13anc 
 |-  ( ( ( ( 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 ) ) ) -> ( f |` ( S \ { x } ) ) e. ( B ^m ( S \ { x } ) ) )
46 id 
 |-  ( g = ( f |` ( S \ { x } ) ) -> g = ( f |` ( S \ { x } ) ) )
47 3 a1i 
 |-  ( g = ( f |` ( S \ { x } ) ) -> .0. = ( 0g ` R ) )
48 46 47 breq12d 
 |-  ( g = ( f |` ( S \ { x } ) ) -> ( g finSupp .0. <-> ( f |` ( S \ { x } ) ) finSupp ( 0g ` R ) ) )
49 48 notbid 
 |-  ( g = ( f |` ( S \ { x } ) ) -> ( -. g finSupp .0. <-> -. ( f |` ( S \ { x } ) ) finSupp ( 0g ` R ) ) )
50 oveq1 
 |-  ( g = ( f |` ( S \ { x } ) ) -> ( g ( linC ` M ) ( S \ { x } ) ) = ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) )
51 50 eqeq2d 
 |-  ( g = ( f |` ( S \ { x } ) ) -> ( ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) <-> ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) ) )
52 51 notbid 
 |-  ( g = ( f |` ( S \ { x } ) ) -> ( -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) <-> -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) ) )
53 49 52 orbi12d 
 |-  ( g = ( f |` ( S \ { x } ) ) -> ( ( -. g finSupp .0. \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) <-> ( -. ( f |` ( S \ { x } ) ) finSupp ( 0g ` R ) \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) ) ) )
54 53 rspcva 
 |-  ( ( ( f |` ( S \ { x } ) ) e. ( B ^m ( S \ { x } ) ) /\ A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) ) -> ( -. ( f |` ( S \ { x } ) ) finSupp ( 0g ` R ) \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) ) )
55 3 breq2i 
 |-  ( f finSupp .0. <-> f finSupp ( 0g ` R ) )
56 55 biimpi 
 |-  ( f finSupp .0. -> f finSupp ( 0g ` R ) )
57 56 adantr 
 |-  ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> f finSupp ( 0g ` R ) )
58 57 adantl 
 |-  ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> f finSupp ( 0g ` R ) )
59 58 adantl 
 |-  ( ( ( ( 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 ) ) ) -> f finSupp ( 0g ` R ) )
60 fvexd 
 |-  ( ( ( ( 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 ) ) ) -> ( 0g ` R ) e. _V )
61 59 60 fsuppres 
 |-  ( ( ( ( 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 ) ) ) -> ( f |` ( S \ { x } ) ) finSupp ( 0g ` R ) )
62 61 pm2.24d 
 |-  ( ( ( ( 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 ) ) ) -> ( -. ( f |` ( S \ { x } ) ) finSupp ( 0g ` R ) -> ( f ` x ) = .0. ) )
63 62 com12 
 |-  ( -. ( f |` ( S \ { x } ) ) finSupp ( 0g ` R ) -> ( ( ( ( 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 ) ) ) -> ( f ` x ) = .0. ) )
64 simplr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> M e. LMod )
65 64 adantr 
 |-  ( ( ( ( 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 e. LMod )
66 1 fveq2i 
 |-  ( Base ` R ) = ( Base ` ( Scalar ` M ) )
67 2 66 eqtr2i 
 |-  ( Base ` ( Scalar ` M ) ) = B
68 67 oveq1i 
 |-  ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { x } ) ) = ( B ^m ( S \ { x } ) )
69 45 68 eleqtrrdi 
 |-  ( ( ( ( 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 ) ) ) -> ( f |` ( S \ { x } ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { x } ) ) )
70 ssdifss 
 |-  ( S C_ ( Base ` M ) -> ( S \ { x } ) C_ ( Base ` M ) )
71 70 adantr 
 |-  ( ( S C_ ( Base ` M ) /\ x e. S ) -> ( S \ { x } ) C_ ( Base ` M ) )
72 71 adantl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( S \ { x } ) C_ ( Base ` M ) )
73 difexg 
 |-  ( S e. V -> ( S \ { x } ) e. _V )
74 73 adantr 
 |-  ( ( S e. V /\ M e. LMod ) -> ( S \ { x } ) e. _V )
75 74 adantr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( S \ { x } ) e. _V )
76 elpwg 
 |-  ( ( S \ { x } ) e. _V -> ( ( S \ { x } ) e. ~P ( Base ` M ) <-> ( S \ { x } ) C_ ( Base ` M ) ) )
77 75 76 syl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( ( S \ { x } ) e. ~P ( Base ` M ) <-> ( S \ { x } ) C_ ( Base ` M ) ) )
78 72 77 mpbird 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ x e. S ) ) -> ( S \ { x } ) e. ~P ( Base ` M ) )
79 78 adantr 
 |-  ( ( ( ( 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 ) ) ) -> ( S \ { x } ) e. ~P ( Base ` M ) )
80 lincval 
 |-  ( ( M e. LMod /\ ( f |` ( S \ { x } ) ) e. ( ( Base ` ( Scalar ` M ) ) ^m ( S \ { x } ) ) /\ ( S \ { x } ) e. ~P ( Base ` M ) ) -> ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) = ( M gsum ( z e. ( S \ { x } ) |-> ( ( ( f |` ( S \ { x } ) ) ` z ) ( .s ` M ) z ) ) ) )
81 65 69 79 80 syl3anc 
 |-  ( ( ( ( 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 ) ) ) -> ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) = ( M gsum ( z e. ( S \ { x } ) |-> ( ( ( f |` ( S \ { x } ) ) ` z ) ( .s ` M ) z ) ) ) )
82 fvres 
 |-  ( z e. ( S \ { x } ) -> ( ( f |` ( S \ { x } ) ) ` z ) = ( f ` z ) )
83 82 adantl 
 |-  ( ( ( ( ( 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 ) ) ) /\ z e. ( S \ { x } ) ) -> ( ( f |` ( S \ { x } ) ) ` z ) = ( f ` z ) )
84 83 oveq1d 
 |-  ( ( ( ( ( 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 ) ) ) /\ z e. ( S \ { x } ) ) -> ( ( ( f |` ( S \ { x } ) ) ` z ) ( .s ` M ) z ) = ( ( f ` z ) ( .s ` M ) z ) )
85 84 mpteq2dva 
 |-  ( ( ( ( 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 ) ) ) -> ( z e. ( S \ { x } ) |-> ( ( ( f |` ( S \ { x } ) ) ` z ) ( .s ` M ) z ) ) = ( z e. ( S \ { x } ) |-> ( ( f ` z ) ( .s ` M ) z ) ) )
86 85 oveq2d 
 |-  ( ( ( ( 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 ( z e. ( S \ { x } ) |-> ( ( ( f |` ( S \ { x } ) ) ` z ) ( .s ` M ) z ) ) ) = ( M gsum ( z e. ( S \ { x } ) |-> ( ( f ` z ) ( .s ` M ) z ) ) ) )
87 simplr 
 |-  ( ( ( ( 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 ) ) ) -> ( S C_ ( Base ` M ) /\ x e. S ) )
88 3anass 
 |-  ( ( f e. ( B ^m S ) /\ f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) <-> ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) )
89 88 bicomi 
 |-  ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) <-> ( f e. ( B ^m S ) /\ f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) )
90 89 biimpi 
 |-  ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( f e. ( B ^m S ) /\ f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) )
91 90 adantl 
 |-  ( ( ( ( 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 ) ) ) -> ( f e. ( B ^m S ) /\ f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) )
92 1 2 3 4 42 43 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 ( z e. ( S \ { x } ) |-> ( ( f ` z ) ( .s ` M ) z ) ) ) = ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) )
93 37 87 91 92 syl3anc 
 |-  ( ( ( ( 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 ( z e. ( S \ { x } ) |-> ( ( f ` z ) ( .s ` M ) z ) ) ) = ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) )
94 81 86 93 3eqtrrd 
 |-  ( ( ( ( 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 ) ) ) -> ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) )
95 94 pm2.24d 
 |-  ( ( ( ( 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 ) ) ) -> ( -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) -> ( f ` x ) = .0. ) )
96 95 com12 
 |-  ( -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) -> ( ( ( ( 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 ) ) ) -> ( f ` x ) = .0. ) )
97 63 96 jaoi 
 |-  ( ( -. ( f |` ( S \ { x } ) ) finSupp ( 0g ` R ) \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( ( f |` ( S \ { x } ) ) ( linC ` M ) ( S \ { x } ) ) ) -> ( ( ( ( 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 ) ) ) -> ( f ` x ) = .0. ) )
98 54 97 syl 
 |-  ( ( ( f |` ( S \ { x } ) ) e. ( B ^m ( S \ { x } ) ) /\ A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) ) -> ( ( ( ( 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 ) ) ) -> ( f ` x ) = .0. ) )
99 98 ex 
 |-  ( ( f |` ( S \ { x } ) ) e. ( B ^m ( S \ { x } ) ) -> ( A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( ( ( ( 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 ) ) ) -> ( f ` x ) = .0. ) ) )
100 99 com23 
 |-  ( ( f |` ( S \ { x } ) ) e. ( B ^m ( S \ { x } ) ) -> ( ( ( ( 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 ) ) ) -> ( A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) ) )
101 45 100 mpcom 
 |-  ( ( ( ( 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 ) ) ) -> ( A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( ( ( invg ` R ) ` ( f ` x ) ) ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) )
102 35 101 syl5 
 |-  ( ( ( ( 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 ) ) ) -> ( ( ( ( invg ` R ) ` ( f ` x ) ) e. ( B \ { .0. } ) /\ A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) ) -> ( f ` x ) = .0. ) )
103 102 expd 
 |-  ( ( ( ( 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 ) ) ) -> ( ( ( invg ` R ) ` ( f ` x ) ) e. ( B \ { .0. } ) -> ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) ) )
104 29 103 syldc 
 |-  ( -. ( f ` x ) = .0. -> ( ( ( ( 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 ) ) ) -> ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) ) )
105 104 expd 
 |-  ( -. ( f ` x ) = .0. -> ( ( ( 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 ) ) -> ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) ) ) )
106 6 105 pm2.61i 
 |-  ( ( ( 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 ) ) -> ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( f ` x ) = .0. ) ) )