Metamath Proof Explorer

Theorem islinindfis

Description: The property of being a linearly independent finite subset. (Contributed by AV, 27-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 islininds.b 
 |-  B = ( Base ` M )
2 islininds.z 
 |-  Z = ( 0g ` M )
3 islininds.r 
 |-  R = ( Scalar ` M )
4 islininds.e 
 |-  E = ( Base ` R )
5 islininds.0 
 |-  .0. = ( 0g ` R )
6 1 2 3 4 5 islininds 
 |-  ( ( S e. Fin /\ 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. ) ) ) )
7 pm4.79 
 |-  ( ( ( f finSupp .0. -> A. x e. S ( f ` x ) = .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. ) )
8 elmapi 
 |-  ( f e. ( E ^m S ) -> f : S --> E )
9 8 adantl 
 |-  ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> f : S --> E )
10 simpll 
 |-  ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> S e. Fin )
11 5 fvexi 
 |-  .0. e. _V
12 11 a1i 
 |-  ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> .0. e. _V )
13 9 10 12 fdmfifsupp 
 |-  ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> f finSupp .0. )
14 13 adantr 
 |-  ( ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) /\ ( f ( linC ` M ) S ) = Z ) -> f finSupp .0. )
15 14 imim1i 
 |-  ( ( f finSupp .0. -> A. x e. S ( f ` x ) = .0. ) -> ( ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) )
16 15 expd 
 |-  ( ( f finSupp .0. -> A. x e. S ( f ` x ) = .0. ) -> ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) )
17 ax-1 
 |-  ( ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) -> ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) )
18 16 17 jaoi 
 |-  ( ( ( f finSupp .0. -> A. x e. S ( f ` x ) = .0. ) \/ ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) -> ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) )
19 7 18 sylbir 
 |-  ( ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) )
20 19 com12 
 |-  ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> ( ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) -> ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) )
21 pm3.42 
 |-  ( ( ( 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 20 21 impbid1 
 |-  ( ( ( S e. Fin /\ M e. W ) /\ f e. ( E ^m S ) ) -> ( ( ( f finSupp .0. /\ ( f ( linC ` M ) S ) = Z ) -> A. x e. S ( f ` x ) = .0. ) <-> ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) )
23 22 ralbidva 
 |-  ( ( S e. Fin /\ M e. W ) -> ( 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 ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) )
24 23 anbi2d 
 |-  ( ( S e. Fin /\ 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. ) ) <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) ) )
25 6 24 bitrd 
 |-  ( ( S e. Fin /\ M e. W ) -> ( S linIndS M <-> ( S e. ~P B /\ A. f e. ( E ^m S ) ( ( f ( linC ` M ) S ) = Z -> A. x e. S ( f ` x ) = .0. ) ) ) )