Metamath Proof Explorer

Theorem islininds2

Description: Implication of being a linearly independent 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 islininds2 
|- ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( S linIndS M -> A. s e. S A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) ) )

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 lindepsnlininds 
 |-  ( ( S e. ~P B /\ M e. LMod ) -> ( S linDepS M <-> -. S linIndS M ) )
7 6 ancoms 
 |-  ( ( M e. LMod /\ S e. ~P B ) -> ( S linDepS M <-> -. S linIndS M ) )
8 7 3adant3 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( S linDepS M <-> -. S linIndS M ) )
9 8 con2bid 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( S linIndS M <-> -. S linDepS M ) )
10 notnotb 
 |-  ( f finSupp .0. <-> -. -. f finSupp .0. )
11 nne 
 |-  ( -. ( f ( linC ` M ) ( S \ { s } ) ) =/= s <-> ( f ( linC ` M ) ( S \ { s } ) ) = s )
12 11 bicomi 
 |-  ( ( f ( linC ` M ) ( S \ { s } ) ) = s <-> -. ( f ( linC ` M ) ( S \ { s } ) ) =/= s )
13 10 12 anbi12i 
 |-  ( ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> ( -. -. f finSupp .0. /\ -. ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) )
14 pm4.56 
 |-  ( ( -. -. f finSupp .0. /\ -. ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) <-> -. ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) )
15 13 14 bitri 
 |-  ( ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> -. ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) )
16 15 rexbii 
 |-  ( E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> E. f e. ( E ^m ( S \ { s } ) ) -. ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) )
17 rexnal 
 |-  ( E. f e. ( E ^m ( S \ { s } ) ) -. ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) <-> -. A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) )
18 16 17 bitri 
 |-  ( E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> -. A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) )
19 18 rexbii 
 |-  ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> E. s e. S -. A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) )
20 rexnal 
 |-  ( E. s e. S -. A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) <-> -. A. s e. S A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) )
21 19 20 bitri 
 |-  ( E. s e. S E. f e. ( E ^m ( S \ { s } ) ) ( f finSupp .0. /\ ( f ( linC ` M ) ( S \ { s } ) ) = s ) <-> -. A. s e. S A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) )
22 1 2 3 4 5 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 ) )
23 21 22 syl5bir 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( -. A. s e. S A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) -> S linDepS M ) )
24 23 con1d 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( -. S linDepS M -> A. s e. S A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) ) )
25 9 24 sylbid 
 |-  ( ( M e. LMod /\ S e. ~P B /\ R e. NzRing ) -> ( S linIndS M -> A. s e. S A. f e. ( E ^m ( S \ { s } ) ) ( -. f finSupp .0. \/ ( f ( linC ` M ) ( S \ { s } ) ) =/= s ) ) )