Metamath Proof Explorer

Theorem lindslinindsimp2

Description: Implication 2 for lindslininds . (Contributed by AV, 26-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 lindslinindsimp2 
|- ( ( S e. V /\ M e. LMod ) -> ( ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) -> ( 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. ) ) ) )

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 simprl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) -> S C_ ( Base ` M ) )
6 elpwg 
 |-  ( S e. V -> ( S e. ~P ( Base ` M ) <-> S C_ ( Base ` M ) ) )
7 6 ad2antrr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) -> ( S e. ~P ( Base ` M ) <-> S C_ ( Base ` M ) ) )
8 5 7 mpbird 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) -> S e. ~P ( Base ` M ) )
9 simplr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> M e. LMod )
10 ssdifss 
 |-  ( S C_ ( Base ` M ) -> ( S \ { s } ) C_ ( Base ` M ) )
11 10 adantl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( S \ { s } ) C_ ( Base ` M ) )
12 difexg 
 |-  ( S e. V -> ( S \ { s } ) e. _V )
13 12 ad2antrr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( S \ { s } ) e. _V )
14 elpwg 
 |-  ( ( S \ { s } ) e. _V -> ( ( S \ { s } ) e. ~P ( Base ` M ) <-> ( S \ { s } ) C_ ( Base ` M ) ) )
15 13 14 syl 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( ( S \ { s } ) e. ~P ( Base ` M ) <-> ( S \ { s } ) C_ ( Base ` M ) ) )
16 11 15 mpbird 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( S \ { s } ) e. ~P ( Base ` M ) )
17 eqid 
 |-  ( Base ` M ) = ( Base ` M )
18 17 lspeqlco 
 |-  ( ( M e. LMod /\ ( S \ { s } ) e. ~P ( Base ` M ) ) -> ( M LinCo ( S \ { s } ) ) = ( ( LSpan ` M ) ` ( S \ { s } ) ) )
19 18 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 } ) ) ) )
20 19 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 } ) ) ) )
21 9 16 20 syl2anc 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) <-> ( y ( .s ` M ) s ) e. ( M LinCo ( S \ { s } ) ) ) )
22 21 notbid 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) <-> -. ( y ( .s ` M ) s ) e. ( M LinCo ( S \ { s } ) ) ) )
23 17 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 } ) ) ) ) ) )
24 3 eqcomi 
 |-  ( 0g ` R ) = .0.
25 24 breq2i 
 |-  ( g finSupp ( 0g ` R ) <-> g finSupp .0. )
26 25 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 } ) ) ) )
27 26 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 } ) ) ) )
28 27 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 } ) ) ) ) )
29 23 28 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 } ) ) ) ) ) )
30 9 16 29 syl2anc 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( 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 } ) ) ) ) ) )
31 30 notbid 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( 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 } ) ) ) ) ) )
32 ianor 
 |-  ( -. ( ( 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 } ) ) ) ) <-> ( -. ( 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 } ) ) ) ) )
33 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 } ) ) ) )
34 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 } ) ) ) )
35 34 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 } ) ) ) )
36 33 35 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 } ) ) ) )
37 36 orbi2i 
 |-  ( ( -. ( 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 } ) ) ) ) <-> ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
38 32 37 bitri 
 |-  ( -. ( ( 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 } ) ) ) ) <-> ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
39 31 38 bitrdi 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( -. ( y ( .s ` M ) s ) e. ( M LinCo ( S \ { s } ) ) <-> ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
40 22 39 bitrd 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) <-> ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
41 40 2ralbidv 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) <-> A. s e. S A. y e. ( B \ { .0. } ) ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
42 simpllr 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> M e. LMod )
43 eldifi 
 |-  ( y e. ( B \ { .0. } ) -> y e. B )
44 43 adantl 
 |-  ( ( s e. S /\ y e. ( B \ { .0. } ) ) -> y e. B )
45 44 adantl 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> y e. B )
46 ssel2 
 |-  ( ( S C_ ( Base ` M ) /\ s e. S ) -> s e. ( Base ` M ) )
47 46 ad2ant2lr 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> s e. ( Base ` M ) )
48 eqid 
 |-  ( .s ` M ) = ( .s ` M )
49 17 1 48 2 lmodvscl 
 |-  ( ( M e. LMod /\ y e. B /\ s e. ( Base ` M ) ) -> ( y ( .s ` M ) s ) e. ( Base ` M ) )
50 42 45 47 49 syl3anc 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( y ( .s ` M ) s ) e. ( Base ` M ) )
51 50 notnotd 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> -. -. ( y ( .s ` M ) s ) e. ( Base ` M ) )
52 nbfal 
 |-  ( -. -. ( y ( .s ` M ) s ) e. ( Base ` M ) <-> ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) <-> F. ) )
53 51 52 sylib 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) <-> F. ) )
54 53 orbi1d 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ ( s e. S /\ y e. ( B \ { .0. } ) ) ) -> ( ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) <-> ( F. \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
55 54 2ralbidva 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( A. s e. S A. y e. ( B \ { .0. } ) ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) <-> A. s e. S A. y e. ( B \ { .0. } ) ( F. \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) ) )
56 r19.32v 
 |-  ( A. y e. ( B \ { .0. } ) ( F. \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) <-> ( F. \/ A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
57 56 ralbii 
 |-  ( A. s e. S A. y e. ( B \ { .0. } ) ( F. \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) <-> A. s e. S ( F. \/ A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
58 r19.32v 
 |-  ( A. s e. S ( F. \/ A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) <-> ( F. \/ A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
59 57 58 bitri 
 |-  ( A. s e. S A. y e. ( B \ { .0. } ) ( F. \/ A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) <-> ( F. \/ A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) )
60 falim 
 |-  ( F. -> ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
61 sneq 
 |-  ( s = x -> { s } = { x } )
62 61 difeq2d 
 |-  ( s = x -> ( S \ { s } ) = ( S \ { x } ) )
63 62 oveq2d 
 |-  ( s = x -> ( B ^m ( S \ { s } ) ) = ( B ^m ( S \ { x } ) ) )
64 oveq2 
 |-  ( s = x -> ( y ( .s ` M ) s ) = ( y ( .s ` M ) x ) )
65 62 oveq2d 
 |-  ( s = x -> ( g ( linC ` M ) ( S \ { s } ) ) = ( g ( linC ` M ) ( S \ { x } ) ) )
66 64 65 eqeq12d 
 |-  ( s = x -> ( ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) <-> ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) )
67 66 notbid 
 |-  ( s = x -> ( -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) <-> -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) )
68 67 orbi2d 
 |-  ( s = x -> ( ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) <-> ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) ) )
69 63 68 raleqbidv 
 |-  ( s = x -> ( 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 \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) ) )
70 69 ralbidv 
 |-  ( s = x -> ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) <-> A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) ) )
71 70 rspcva 
 |-  ( ( x e. S /\ A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) -> A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) )
72 1 2 3 4 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. ) ) )
73 72 expr 
 |-  ( ( ( 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. ) ) ) )
74 73 com14 
 |-  ( A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { x } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) x ) = ( g ( linC ` M ) ( S \ { x } ) ) ) -> ( x e. S -> ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( f ` x ) = .0. ) ) ) )
75 71 74 syl 
 |-  ( ( x e. S /\ A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) -> ( x e. S -> ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( f ` x ) = .0. ) ) ) )
76 75 ex 
 |-  ( x e. S -> ( A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) -> ( x e. S -> ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( f ` x ) = .0. ) ) ) ) )
77 76 pm2.43a 
 |-  ( x e. S -> ( A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) -> ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( f ` x ) = .0. ) ) ) )
78 77 com14 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) -> ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( x e. S -> ( f ` x ) = .0. ) ) ) )
79 78 imp 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) -> ( ( f e. ( B ^m S ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) ) -> ( x e. S -> ( f ` x ) = .0. ) ) )
80 79 expdimp 
 |-  ( ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) /\ f e. ( B ^m S ) ) -> ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> ( x e. S -> ( f ` x ) = .0. ) ) )
81 80 ralrimdv 
 |-  ( ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) /\ f e. ( B ^m S ) ) -> ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) )
82 81 ralrimiva 
 |-  ( ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) /\ A. s e. S A. y e. ( B \ { .0. } ) A. 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. ) )
83 82 expcom 
 |-  ( A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) -> ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
84 60 83 jaoi 
 |-  ( ( F. \/ A. s e. S A. y e. ( B \ { .0. } ) A. g e. ( B ^m ( S \ { s } ) ) ( -. g finSupp .0. \/ -. ( y ( .s ` M ) s ) = ( g ( linC ` M ) ( S \ { s } ) ) ) ) -> ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
85 84 com12 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( ( F. \/ A. s e. S A. y e. ( B \ { .0. } ) A. 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. ) ) )
86 59 85 syl5bi 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( A. s e. S A. y e. ( B \ { .0. } ) ( F. \/ A. 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. ) ) )
87 55 86 sylbid 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( A. s e. S A. y e. ( B \ { .0. } ) ( -. ( y ( .s ` M ) s ) e. ( Base ` M ) \/ A. 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. ) ) )
88 41 87 sylbid 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ S C_ ( Base ` M ) ) -> ( A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) -> A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
89 88 impr 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) -> A. f e. ( B ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) )
90 8 89 jca 
 |-  ( ( ( S e. V /\ M e. LMod ) /\ ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) ) -> ( 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. ) ) )
91 90 ex 
 |-  ( ( S e. V /\ M e. LMod ) -> ( ( S C_ ( Base ` M ) /\ A. s e. S A. y e. ( B \ { .0. } ) -. ( y ( .s ` M ) s ) e. ( ( LSpan ` M ) ` ( S \ { s } ) ) ) -> ( 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. ) ) ) )