Metamath Proof Explorer

Theorem lindslinindsimp1

Description: Implication 1 for lindslininds . (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 )
Assertion lindslinindsimp1 
|- ( ( S e. V /\ M e. LMod ) -> ( ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) -> ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) )

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 elpwi 
 |-  ( S e. ~P ( Base ` M ) -> S C_ ( Base ` M ) )
6 5 ad2antrl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> S C_ ( Base ` M ) )
7 simpr 
 |-  ( ( S e. V /\ M e. LMod ) -> M e. LMod )
8 7 anim2i 
 |-  ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) -> ( S e. ~P ( Base ` M ) /\ M e. LMod ) )
9 8 ancomd 
 |-  ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) -> ( M e. LMod /\ S e. ~P ( Base ` M ) ) )
10 9 ad2antrr 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( M e. LMod /\ S e. ~P ( Base ` M ) ) )
11 eldifi 
 |-  ( y e. ( B \ { .0. } ) -> y e. B )
12 11 adantl 
 |-  ( ( s e. S /\ y e. ( B \ { .0. } ) ) -> y e. B )
13 12 adantl 
 |-  ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> y e. B )
14 13 adantr 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> y e. B )
15 simprl 
 |-  ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> s e. S )
16 15 adantr 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> s e. S )
17 simprl 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> g e. ( B ^m ( S \ { s } ) ) )
18 14 16 17 3jca 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( y e. B /\ s e. S /\ g e. ( B ^m ( S \ { s } ) ) ) )
19 simprrl 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> g finSupp .0. )
20 eqid 
 |-  ( Base ` M ) = ( Base ` M )
21 eqid 
 |-  ( invg ` R ) = ( invg ` R )
22 eqid 
 |-  ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) )
23 20 1 2 3 4 21 22 lincext2 
 |-  ( ( ( M e. LMod /\ S e. ~P ( Base ` M ) ) /\ ( y e. B /\ s e. S /\ g e. ( B ^m ( S \ { s } ) ) ) /\ g finSupp .0. ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) finSupp .0. )
24 10 18 19 23 syl3anc 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) finSupp .0. )
25 8 adantr 
 |-  ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( S e. ~P ( Base ` M ) /\ M e. LMod ) )
26 25 ancomd 
 |-  ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( M e. LMod /\ S e. ~P ( Base ` M ) ) )
27 26 adantr 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( M e. LMod /\ S e. ~P ( Base ` M ) ) )
28 20 1 2 3 4 21 22 lincext1 
 |-  ( ( ( M e. LMod /\ S e. ~P ( Base ` M ) ) /\ ( y e. B /\ s e. S /\ g e. ( B ^m ( S \ { s } ) ) ) ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) e. ( B ^m S ) )
29 27 18 28 syl2anc 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) e. ( B ^m S ) )
30 breq1 
 |-  ( f = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) -> ( f finSupp .0. <-> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) finSupp .0. ) )
31 oveq1 
 |-  ( f = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) -> ( f ( linC ` M ) S ) = ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) )
32 31 eqeq1d 
 |-  ( f = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) -> ( ( f ( linC ` M ) S ) = Z <-> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z ) )
33 30 32 anbi12d 
 |-  ( f = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) -> ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) <-> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) finSupp .0. /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z ) ) )
34 fveq1 
 |-  ( f = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) -> ( f ` x ) = ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) )
35 34 eqeq1d 
 |-  ( f = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) -> ( ( f ` x ) = .0. <-> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. ) )
36 35 ralbidv 
 |-  ( f = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) -> ( A. x e. S ( f ` x ) = .0. <-> A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. ) )
37 33 36 imbi12d 
 |-  ( f = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) -> ( ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) finSupp .0. /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z ) -> A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. ) ) )
38 37 rspcv 
 |-  ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) e. ( B ^m S ) -> ( A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) finSupp .0. /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z ) -> A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. ) ) )
39 29 38 syl 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) finSupp .0. /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z ) -> A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. ) ) )
40 39 exp4a 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) finSupp .0. -> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z -> A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. ) ) ) )
41 24 40 mpid 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z -> A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. ) ) )
42 simprr 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
43 20 1 2 3 4 21 22 lincext3 
 |-  ( ( ( M e. LMod /\ S e. ~P ( Base ` M ) ) /\ ( y e. B /\ s e. S /\ g e. ( B ^m ( S \ { s } ) ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z )
44 10 18 42 43 syl3anc 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z )
45 fveqeq2 
 |-  ( x = s -> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. <-> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` s ) = .0. ) )
46 45 rspcv 
 |-  ( s e. S -> ( A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` s ) = .0. ) )
47 16 46 syl 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` s ) = .0. ) )
48 eqidd 
 |-  ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) )
49 iftrue 
 |-  ( z = s -> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) = ( ( invg ` R ) ` y ) )
50 49 adantl 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ z = s ) -> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) = ( ( invg ` R ) ` y ) )
51 fvexd 
 |-  ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( ( invg ` R ) ` y ) e. _V )
52 48 50 15 51 fvmptd 
 |-  ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` s ) = ( ( invg ` R ) ` y ) )
53 52 adantr 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` s ) = ( ( invg ` R ) ` y ) )
54 53 eqeq1d 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` s ) = .0. <-> ( ( invg ` R ) ` y ) = .0. ) )
55 1 lmodfgrp 
 |-  ( M e. LMod -> R e. Grp )
56 2 3 21 grpinvnzcl 
 |-  ( ( R e. Grp /\ y e. ( B \ { .0. } ) ) -> ( ( invg ` R ) ` y ) e. ( B \ { .0. } ) )
57 eldif 
 |-  ( ( ( invg ` R ) ` y ) e. ( B \ { .0. } ) <-> ( ( ( invg ` R ) ` y ) e. B /\ -. ( ( invg ` R ) ` y ) e. { .0. } ) )
58 fvex 
 |-  ( ( invg ` R ) ` y ) e. _V
59 58 elsn 
 |-  ( ( ( invg ` R ) ` y ) e. { .0. } <-> ( ( invg ` R ) ` y ) = .0. )
60 pm2.21 
 |-  ( -. ( ( invg ` R ) ` y ) = .0. -> ( ( ( invg ` R ) ` y ) = .0. -> ( S e. V -> ( s e. S -> ( S e. ~P ( Base ` M ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) )
61 60 com25 
 |-  ( -. ( ( invg ` R ) ` y ) = .0. -> ( S e. ~P ( Base ` M ) -> ( S e. V -> ( s e. S -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) )
62 59 61 sylnbi 
 |-  ( -. ( ( invg ` R ) ` y ) e. { .0. } -> ( S e. ~P ( Base ` M ) -> ( S e. V -> ( s e. S -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) )
63 57 62 simplbiim 
 |-  ( ( ( invg ` R ) ` y ) e. ( B \ { .0. } ) -> ( S e. ~P ( Base ` M ) -> ( S e. V -> ( s e. S -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) )
64 56 63 syl 
 |-  ( ( R e. Grp /\ y e. ( B \ { .0. } ) ) -> ( S e. ~P ( Base ` M ) -> ( S e. V -> ( s e. S -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) )
65 64 ex 
 |-  ( R e. Grp -> ( y e. ( B \ { .0. } ) -> ( S e. ~P ( Base ` M ) -> ( S e. V -> ( s e. S -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) ) )
66 55 65 syl 
 |-  ( M e. LMod -> ( y e. ( B \ { .0. } ) -> ( S e. ~P ( Base ` M ) -> ( S e. V -> ( s e. S -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) ) )
67 66 com24 
 |-  ( M e. LMod -> ( S e. V -> ( S e. ~P ( Base ` M ) -> ( y e. ( B \ { .0. } ) -> ( s e. S -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) ) )
68 67 impcom 
 |-  ( ( S e. V /\ M e. LMod ) -> ( S e. ~P ( Base ` M ) -> ( y e. ( B \ { .0. } ) -> ( s e. S -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) )
69 68 impcom 
 |-  ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) -> ( y e. ( B \ { .0. } ) -> ( s e. S -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
70 69 com13 
 |-  ( s e. S -> ( y e. ( B \ { .0. } ) -> ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
71 70 imp 
 |-  ( ( s e. S /\ y e. ( B \ { .0. } ) ) -> ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
72 71 impcom 
 |-  ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
73 72 adantr 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( ( ( invg ` R ) ` y ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
74 54 73 sylbid 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` s ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
75 47 74 syld 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
76 44 75 embantd 
 |-  ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> ( ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ( linC ` M ) S ) = Z -> A. x e. S ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` y ) , ( g ` z ) ) ) ` x ) = .0. ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
77 41 76 syldc 
 |-  ( A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( ( ( ( S e. ~P ( Base ` M ) /\ ( S e. V /\ M e. LMod ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
78 77 exp5j 
 |-  ( A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( S e. ~P ( Base ` M ) -> ( ( S e. V /\ M e. LMod ) -> ( ( s e. S /\ y e. ( B \ { .0. } ) ) -> ( ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) ) )
79 78 impcom 
 |-  ( ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) -> ( ( S e. V /\ M e. LMod ) -> ( ( s e. S /\ y e. ( B \ { .0. } ) ) -> ( ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
80 79 impcom 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> ( ( s e. S /\ y e. ( B \ { .0. } ) ) -> ( ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
81 80 imp 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( ( g e. ( B ^m ( S \ { s } ) ) /\ ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
82 81 expdimp 
 |-  ( ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ g e. ( B ^m ( S \ { s } ) ) ) -> ( ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
83 82 expd 
 |-  ( ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ g e. ( B ^m ( S \ { s } ) ) ) -> ( g finSupp .0. -> ( ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
84 83 impcom 
 |-  ( ( g finSupp .0. /\ ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ g e. ( B ^m ( S \ { s } ) ) ) ) -> ( ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
85 84 pm2.01d 
 |-  ( ( g finSupp .0. /\ ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ g e. ( B ^m ( S \ { s } ) ) ) ) -> -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) )
86 85 olcd 
 |-  ( ( g finSupp .0. /\ ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ g e. ( B ^m ( S \ { s } ) ) ) ) -> ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
87 animorl 
 |-  ( ( -. g finSupp .0. /\ ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ g e. ( B ^m ( S \ { s } ) ) ) ) -> ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
88 86 87 pm2.61ian 
 |-  ( ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) /\ g e. ( B ^m ( S \ { s } ) ) ) -> ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
89 88 ralrimiva 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
90 ralnex 
 |-  ( A. g e. ( B ^m ( S \ { s } ) ) -. ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) <-> -. E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
91 ianor 
 |-  ( -. ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) <-> ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
92 91 ralbii 
 |-  ( A. g e. ( B ^m ( S \ { s } ) ) -. ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) <-> A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
93 90 92 bitr3i 
 |-  ( -. E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) <-> A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
94 89 93 sylibr 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> -. E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
95 94 intnand 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> -. ( ( y ( .s ` M ) s ) e. ( Base ` M ) /\ E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
96 7 ad2antrr 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> M e. LMod )
97 difexg 
 |-  ( S e. V -> ( S \ { s } ) e. _V )
98 97 ad2antrr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> ( S \ { s } ) e. _V )
99 5 ssdifssd 
 |-  ( S e. ~P ( Base ` M ) -> ( S \ { s } ) C_ ( Base ` M ) )
100 99 ad2antrl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> ( S \ { s } ) C_ ( Base ` M ) )
101 98 100 elpwd 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> ( S \ { s } ) e. ~P ( Base ` M ) )
102 101 adantr 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( S \ { s } ) e. ~P ( Base ` M ) )
103 20 lspeqlco 
 |-  ( ( M e. LMod /\ ( S \ { s } ) e. ~P ( Base ` M ) ) -> ( M LinCo ( S \ { s } ) ) = ( ( LSpan ` M ) ` ( S \ { s } ) ) )
104 103 eleq2d 
 |-  ( ( M e. LMod /\ ( S \ { s } ) e. ~P ( Base ` M ) ) -> ( ( y ( .s ` M ) s ) e. ( M LinCo ( S \ { s } ) ) <-> ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) )
105 104 bicomd 
 |-  ( ( M e. LMod /\ ( S \ { s } ) e. ~P ( Base ` M ) ) -> ( ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) <-> ( y ( .s ` M ) s ) e. ( M LinCo ( S \ { s } ) ) ) )
106 96 102 105 syl2anc 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) <-> ( y ( .s ` M ) s ) e. ( M LinCo ( S \ { s } ) ) ) )
107 7 adantr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> M e. LMod )
108 difexg 
 |-  ( S e. ~P ( Base ` M ) -> ( S \ { s } ) e. _V )
109 108 99 elpwd 
 |-  ( S e. ~P ( Base ` M ) -> ( S \ { s } ) e. ~P ( Base ` M ) )
110 109 ad2antrl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> ( S \ { s } ) e. ~P ( Base ` M ) )
111 107 110 jca 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> ( M e. LMod /\ ( S \ { s } ) e. ~P ( Base ` M ) ) )
112 111 adantr 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( M e. LMod /\ ( S \ { s } ) e. ~P ( Base ` M ) ) )
113 20 1 2 lcoval 
 |-  ( ( M e. LMod /\ ( S \ { s } ) e. ~P ( Base ` M ) ) -> ( ( y ( .s ` M ) s ) e. ( M LinCo ( S \ { s } ) ) <-> ( ( y ( .s ` M ) s ) e. ( Base ` M ) /\ E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp ( 0g ` R ) /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
114 3 eqcomi 
 |-  ( 0g ` R ) = .0.
115 114 breq2i 
 |-  ( g finSupp ( 0g ` R ) <-> g finSupp .0. )
116 115 anbi1i 
 |-  ( ( g finSupp ( 0g ` R ) /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) <-> ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
117 116 rexbii 
 |-  ( E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp ( 0g ` R ) /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) <-> E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) )
118 117 anbi2i 
 |-  ( ( ( y ( .s ` M ) s ) e. ( Base ` M ) /\ E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp ( 0g ` R ) /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) <-> ( ( y ( .s ` M ) s ) e. ( Base ` M ) /\ E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
119 113 118 bitrdi 
 |-  ( ( M e. LMod /\ ( S \ { s } ) e. ~P ( Base ` M ) ) -> ( ( y ( .s ` M ) s ) e. ( M LinCo ( S \ { s } ) ) <-> ( ( y ( .s ` M ) s ) e. ( Base ` M ) /\ E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
120 112 119 syl 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( ( y ( .s ` M ) s ) e. ( M LinCo ( S \ { s } ) ) <-> ( ( y ( .s ` M ) s ) e. ( Base ` M ) /\ E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
121 106 120 bitrd 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) <-> ( ( y ( .s ` M ) s ) e. ( Base ` M ) /\ E. g e. ( B ^m ( S \ { s } ) ) ( g finSupp .0. /\ ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
122 95 121 mtbird 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) )
123 122 ralrimivva 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) )
124 6 123 jca 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) -> ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) )
125 124 ex 
 |-  ( ( S e. V /\ M e. LMod ) -> ( ( S e. ~P ( Base ` M ) /\ A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) -> ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) )