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 ) )`
` |-  ( ( 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 ) ) )`