Metamath Proof Explorer

Theorem islindeps2

Description: Conditions for being a linearly dependent subset of a (left) module over a nonzero ring. (Contributed by AV, 29-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Hypotheses islindeps2.b 
|- B = ( Base ` M )
islindeps2.z 
|- Z = ( 0g ` M )
islindeps2.r 
|- R = ( Scalar ` M )
islindeps2.e 
|- E = ( Base ` R )
islindeps2.0 
|- .0. = ( 0g ` R )
Assertion islindeps2 
|- ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) -> S linDepS M ) )

Proof

Step Hyp Ref Expression
1 islindeps2.b 
 |-  B = ( Base ` M )
2 islindeps2.z 
 |-  Z = ( 0g ` M )
3 islindeps2.r 
 |-  R = ( Scalar ` M )
4 islindeps2.e 
 |-  E = ( Base ` R )
5 islindeps2.0 
 |-  .0. = ( 0g ` R )
6 id 
 |-  ( ( M e. LMod /\ S e. ~P B ) -> ( M e. LMod /\ S e. ~P B ) )
7 6 3adant3 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( M e. LMod /\ S e. ~P B ) )
8 7 ad3antrrr 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( M e. LMod /\ S e. ~P B ) )
9 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
10 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
11 4 10 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. E )
12 9 11 syl 
 |-  ( R e. NzRing -> ( 1r ` R ) e. E )
13 12 3ad2ant3 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( 1r ` R ) e. E )
14 13 ad3antrrr 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( 1r ` R ) e. E )
15 simpllr 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> s e. S )
16 simplr 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> f e. ( E ^m ( S \ { s } ) ) )
17 14 15 16 3jca 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( ( 1r ` R ) e. E /\ s e. S /\ f e. ( E ^m ( S \ { s } ) ) ) )
18 simprl 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> f finSupp .0. )
19 eqid 
 |-  ( invg ` R ) = ( invg ` R )
20 eqid 
 |-  ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) )
21 1 3 4 5 2 19 20 lincext2 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( ( 1r ` R ) e. E /\ s e. S /\ f e. ( E ^m ( S \ { s } ) ) ) /\ f finSupp .0. ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) finSupp .0. )
22 8 17 18 21 syl3anc 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) finSupp .0. )
23 simpl1 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> M e. LMod )
24 elelpwi 
 |-  ( ( s e. S /\ S e. ~P B ) -> s e. B )
25 24 expcom 
 |-  ( S e. ~P B -> ( s e. S -> s e. B ) )
26 25 3ad2ant2 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( s e. S -> s e. B ) )
27 26 imp 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> s e. B )
28 eqid 
 |-  ( .s ` M ) = ( .s ` M )
29 1 3 28 10 lmodvs1 
 |-  ( ( M e. LMod /\ s e. B ) -> ( ( 1r ` R ) ( .s ` M ) s ) = s )
30 23 27 29 syl2anc 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> ( ( 1r ` R ) ( .s ` M ) s ) = s )
31 30 adantr 
 |-  ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) -> ( ( 1r ` R ) ( .s ` M ) s ) = s )
32 id 
 |-  ( ( f ( linC ` M ) ( S \ { s } ) ) = s -> ( f ( linC ` M ) ( S \ { s } ) ) = s )
33 32 eqcomd 
 |-  ( ( f ( linC ` M ) ( S \ { s } ) ) = s -> s = ( f ( linC ` M ) ( S \ { s } ) ) )
34 33 adantl 
 |-  ( ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) -> s = ( f ( linC ` M ) ( S \ { s } ) ) )
35 31 34 sylan9eq 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( ( 1r ` R ) ( .s ` M ) s ) = ( f ( linC ` M ) ( S \ { s } ) ) )
36 1 3 4 5 2 19 20 lincext3 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( ( 1r ` R ) e. E /\ s e. S /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( ( 1r ` R ) ( .s ` M ) s ) = ( f ( linC ` M ) ( S \ { s } ) ) ) ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ( linC ` M ) S ) = Z )
37 8 17 18 35 36 syl112anc 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ( linC ` M ) S ) = Z )
38 22 37 jca 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) finSupp .0. /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ( linC ` M ) S ) = Z ) )
39 eqidd 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) )
40 iftrue 
 |-  ( z = s -> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) = ( ( invg ` R ) ` ( 1r ` R ) ) )
41 40 adantl 
 |-  ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ z = s ) -> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) = ( ( invg ` R ) ` ( 1r ` R ) ) )
42 simpr 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> s e. S )
43 fvexd 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> ( ( invg ` R ) ` ( 1r ` R ) ) e. _V )
44 39 41 42 43 fvmptd 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ` s ) = ( ( invg ` R ) ` ( 1r ` R ) ) )
45 nzrneg1ne0 
 |-  ( R e. NzRing -> ( ( invg ` R ) ` ( 1r ` R ) ) =/= ( 0g ` R ) )
46 5 a1i 
 |-  ( R e. NzRing -> .0. = ( 0g ` R ) )
47 45 46 neeqtrrd 
 |-  ( R e. NzRing -> ( ( invg ` R ) ` ( 1r ` R ) ) =/= .0. )
48 47 3ad2ant3 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( ( invg ` R ) ` ( 1r ` R ) ) =/= .0. )
49 48 adantr 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> ( ( invg ` R ) ` ( 1r ` R ) ) =/= .0. )
50 44 49 eqnetrd 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ` s ) =/= .0. )
51 50 adantr 
 |-  ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ` s ) =/= .0. )
52 51 adantr 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ` s ) =/= .0. )
53 1 3 4 5 2 19 20 lincext1 
 |-  ( ( ( M e. LMod /\ S e. ~P B ) /\ ( ( 1r ` R ) e. E /\ s e. S /\ f e. ( E ^m ( S \ { s } ) ) ) ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) e. ( E ^m S ) )
54 8 17 53 syl2anc 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) e. ( E ^m S ) )
55 breq1 
 |-  ( g = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) -> ( g finSupp .0. <-> ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) finSupp .0. ) )
56 oveq1 
 |-  ( g = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) -> ( g ( linC ` M ) S ) = ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ( linC ` M ) S ) )
57 56 eqeq1d 
 |-  ( g = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) -> ( ( g ( linC ` M ) S ) = Z <-> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ( linC ` M ) S ) = Z ) )
58 55 57 anbi12d 
 |-  ( g = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) -> ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) <-> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) finSupp .0. /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ( linC ` M ) S ) = Z ) ) )
59 fveq1 
 |-  ( g = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) -> ( g ` s ) = ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ` s ) )
60 59 neeq1d 
 |-  ( g = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) -> ( ( g ` s ) =/= .0. <-> ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ` s ) =/= .0. ) )
61 58 60 anbi12d 
 |-  ( g = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) -> ( ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) <-> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) finSupp .0. /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ( linC ` M ) S ) = Z ) /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ` s ) =/= .0. ) ) )
62 61 adantl 
 |-  ( ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) /\ g = ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ) -> ( ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) <-> ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) finSupp .0. /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ( linC ` M ) S ) = Z ) /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ` s ) =/= .0. ) ) )
63 54 62 rspcedv 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( ( ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) finSupp .0. /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ( linC ` M ) S ) = Z ) /\ ( ( z e. S |-> if ( z = s , ( ( invg ` R ) ` ( 1r ` R ) ) , ( f ` z ) ) ) ` s ) =/= .0. ) -> E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) )
64 38 52 63 mp2and 
 |-  ( ( ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) /\ f e. ( E ^m ( S \ { s } ) ) ) /\ ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
65 64 rexlimdva2 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ s e. S ) -> ( E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) -> E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) )
66 65 reximdva 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) -> E. s e. S E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) ) )
67 66 imp 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> E. s e. S E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
68 df-3an 
 |-  ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) <-> ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ E. s e. S ( g ` s ) =/= .0. ) )
69 r19.42v 
 |-  ( E. s e. S ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) <-> ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ E. s e. S ( g ` s ) =/= .0. ) )
70 68 69 bitr4i 
 |-  ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) <-> E. s e. S ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
71 70 rexbii 
 |-  ( E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) <-> E. g e. ( E ^m S ) E. s e. S ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
72 rexcom 
 |-  ( E. g e. ( E ^m S ) E. s e. S ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) <-> E. s e. S E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
73 71 72 bitri 
 |-  ( E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) <-> E. s e. S E. g e. ( E ^m S ) ( ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z ) /\ ( g ` s ) =/= .0. ) )
74 67 73 sylibr 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) )
75 1 2 3 4 5 islindeps 
 |-  ( ( M e. LMod /\ S e. ~P B ) -> ( S linDepS M <-> E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) ) )
76 75 3adant3 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( S linDepS M <-> E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) ) )
77 76 adantr 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> ( S linDepS M <-> E. g e. ( E ^m S ) ( g finSupp .0. /\ ( g ( linC ` M ) S ) = Z /\ E. s e. S ( g ` s ) =/= .0. ) ) )
78 74 77 mpbird 
 |-  ( ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) /\ E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) ) -> S linDepS M )
79 78 ex 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) -> S linDepS M ) )