Metamath Proof Explorer

Theorem islindeps

Description: The property of being a linearly dependent subset. (Contributed by AV, 26-Apr-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Hypotheses islindeps.b 
|- B = ( Base ` M )
islindeps.z 
|- Z = ( 0g ` M )
islindeps.r 
|- R = ( Scalar ` M )
islindeps.e 
|- E = ( Base ` R )
islindeps.0 
|- .0. = ( 0g ` R )
Assertion islindeps 
|- ( ( M e. W /\ S e. ~P B ) -> ( S linDepS M <-> E. f e. ( E ^m S ) ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z /\ E. x e. S ( f ` x ) =/= .0. ) ) )

Proof

Step Hyp Ref Expression
1 islindeps.b 
 |-  B = ( Base ` M )
2 islindeps.z 
 |-  Z = ( 0g ` M )
3 islindeps.r 
 |-  R = ( Scalar ` M )
4 islindeps.e 
 |-  E = ( Base ` R )
5 islindeps.0 
 |-  .0. = ( 0g ` R )
6 lindepsnlininds 
 |-  ( ( S e. ~P B /\ M e. W ) -> ( S linDepS M <-> -. S linIndS M ) )
7 6 ancoms 
 |-  ( ( M e. W /\ S e. ~P B ) -> ( S linDepS M <-> -. S linIndS M ) )
8 1 2 3 4 5 islininds 
 |-  ( ( S e. ~P B /\ M e. W ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) )
9 8 ancoms 
 |-  ( ( M e. W /\ S e. ~P B ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) )
10 ibar 
 |-  ( S e. ~P B -> ( A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) ) )
11 10 bicomd 
 |-  ( S e. ~P B -> ( ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) <-> A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
12 11 adantl 
 |-  ( ( M e. W /\ S e. ~P B ) -> ( ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) <-> A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
13 9 12 bitrd 
 |-  ( ( M e. W /\ S e. ~P B ) -> ( S linIndS M <-> A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
14 13 notbid 
 |-  ( ( M e. W /\ S e. ~P B ) -> ( -. S linIndS M <-> -. A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) ) )
15 rexnal 
 |-  ( E. f e. ( E ^m S ) -. ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> -. A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) )
16 df-ne 
 |-  ( ( f ` x ) =/= .0. <-> -. ( f ` x ) = .0. )
17 16 rexbii 
 |-  ( E. x e. S ( f ` x ) =/= .0. <-> E. x e. S -. ( f ` x ) = .0. )
18 rexnal 
 |-  ( E. x e. S -. ( f ` x ) = .0. <-> -. A. x e. S ( f ` x ) = .0. )
19 17 18 bitr2i 
 |-  ( -. A. x e. S ( f ` x ) = .0. <-> E. x e. S ( f ` x ) =/= .0. )
20 19 anbi2i 
 |-  ( ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) /\ -. A. x e. S ( f ` x ) = .0. ) <-> ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) /\ E. x e. S ( f ` x ) =/= .0. ) )
21 pm4.61 
 |-  ( -. ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) /\ -. A. x e. S ( f ` x ) = .0. ) )
22 df-3an 
 |-  ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z /\ E. x e. S ( f ` x ) =/= .0. ) <-> ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) /\ E. x e. S ( f ` x ) =/= .0. ) )
23 20 21 22 3bitr4i 
 |-  ( -. ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z /\ E. x e. S ( f ` x ) =/= .0. ) )
24 23 rexbii 
 |-  ( E. f e. ( E ^m S ) -. ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> E. f e. ( E ^m S ) ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z /\ E. x e. S ( f ` x ) =/= .0. ) )
25 15 24 bitr3i 
 |-  ( -. A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> E. f e. ( E ^m S ) ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z /\ E. x e. S ( f ` x ) =/= .0. ) )
26 25 a1i 
 |-  ( ( M e. W /\ S e. ~P B ) -> ( -. A. f e. ( E ^m S ) ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> E. f e. ( E ^m S ) ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z /\ E. x e. S ( f ` x ) =/= .0. ) ) )
27 7 14 26 3bitrd 
 |-  ( ( M e. W /\ S e. ~P B ) -> ( S linDepS M <-> E. f e. ( E ^m S ) ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z /\ E. x e. S ( f ` x ) =/= .0. ) ) )