Metamath Proof Explorer

Theorem linds0

Description: The empty set is always a linearly independent subset. (Contributed by AV, 13-Apr-2019) (Revised by AV, 27-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion linds0 
|- ( M e. V -> (/) linIndS M )

Proof

Step Hyp Ref Expression
1 ral0 
 |-  A. x e. (/) ( (/) ` x ) = ( 0g ` ( Scalar ` M ) )
2 1 2a1i 
 |-  ( M e. V -> ( ( (/) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( (/) ` x ) = ( 0g ` ( Scalar ` M ) ) ) )
3 0ex 
 |-  (/) e. _V
4 breq1 
 |-  ( f = (/) -> ( f finSupp ( 0g ` ( Scalar ` M ) ) <-> (/) finSupp ( 0g ` ( Scalar ` M ) ) ) )
5 oveq1 
 |-  ( f = (/) -> ( f ( linC ` M ) (/) ) = ( (/) ( linC ` M ) (/) ) )
6 5 eqeq1d 
 |-  ( f = (/) -> ( ( f ( linC ` M ) (/) ) = ( 0g ` M ) <-> ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) ) )
7 4 6 anbi12d 
 |-  ( f = (/) -> ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) <-> ( (/) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) ) ) )
8 fveq1 
 |-  ( f = (/) -> ( f ` x ) = ( (/) ` x ) )
9 8 eqeq1d 
 |-  ( f = (/) -> ( ( f ` x ) = ( 0g ` ( Scalar ` M ) ) <-> ( (/) ` x ) = ( 0g ` ( Scalar ` M ) ) ) )
10 9 ralbidv 
 |-  ( f = (/) -> ( A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) <-> A. x e. (/) ( (/) ` x ) = ( 0g ` ( Scalar ` M ) ) ) )
11 7 10 imbi12d 
 |-  ( f = (/) -> ( ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) <-> ( ( (/) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( (/) ` x ) = ( 0g ` ( Scalar ` M ) ) ) ) )
12 11 ralsng 
 |-  ( (/) e. _V -> ( A. f e. { (/) } ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) <-> ( ( (/) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( (/) ` x ) = ( 0g ` ( Scalar ` M ) ) ) ) )
13 3 12 mp1i 
 |-  ( M e. V -> ( A. f e. { (/) } ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) <-> ( ( (/) finSupp ( 0g ` ( Scalar ` M ) ) /\ ( (/) ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( (/) ` x ) = ( 0g ` ( Scalar ` M ) ) ) ) )
14 2 13 mpbird 
 |-  ( M e. V -> A. f e. { (/) } ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) )
15 fvex 
 |-  ( Base ` ( Scalar ` M ) ) e. _V
16 map0e 
 |-  ( ( Base ` ( Scalar ` M ) ) e. _V -> ( ( Base ` ( Scalar ` M ) ) ^m (/) ) = 1o )
17 15 16 mp1i 
 |-  ( M e. V -> ( ( Base ` ( Scalar ` M ) ) ^m (/) ) = 1o )
18 df1o2 
 |-  1o = { (/) }
19 17 18 eqtrdi 
 |-  ( M e. V -> ( ( Base ` ( Scalar ` M ) ) ^m (/) ) = { (/) } )
20 19 raleqdv 
 |-  ( M e. V -> ( A. f e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) <-> A. f e. { (/) } ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) ) )
21 14 20 mpbird 
 |-  ( M e. V -> A. f e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) )
22 0elpw 
 |-  (/) e. ~P ( Base ` M )
23 21 22 jctil 
 |-  ( M e. V -> ( (/) e. ~P ( Base ` M ) /\ A. f e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) ) )
24 eqid 
 |-  ( Base ` M ) = ( Base ` M )
25 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
26 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
27 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
28 eqid 
 |-  ( 0g ` ( Scalar ` M ) ) = ( 0g ` ( Scalar ` M ) )
29 24 25 26 27 28 islininds 
 |-  ( ( (/) e. _V /\ M e. V ) -> ( (/) linIndS M <-> ( (/) e. ~P ( Base ` M ) /\ A. f e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) ) ) )
30 3 29 mpan 
 |-  ( M e. V -> ( (/) linIndS M <-> ( (/) e. ~P ( Base ` M ) /\ A. f e. ( ( Base ` ( Scalar ` M ) ) ^m (/) ) ( ( f finSupp ( 0g ` ( Scalar ` M ) ) /\ ( f ( linC ` M ) (/) ) = ( 0g ` M ) ) -> A. x e. (/) ( f ` x ) = ( 0g ` ( Scalar ` M ) ) ) ) ) )
31 23 30 mpbird 
 |-  ( M e. V -> (/) linIndS M )