Metamath Proof Explorer

Theorem ldepslinc

Description: For (left) vector spaces, isldepslvec2 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc indicates that there is not an analogous alternative definition for arbitrary (left) modules. (Contributed by AV, 25-May-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Assertion ldepslinc 
|- ( A. m e. LVec A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) /\ -. A. m e. LMod A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` m ) = ( Base ` m )
2 eqid 
 |-  ( 0g ` m ) = ( 0g ` m )
3 eqid 
 |-  ( Scalar ` m ) = ( Scalar ` m )
4 eqid 
 |-  ( Base ` ( Scalar ` m ) ) = ( Base ` ( Scalar ` m ) )
5 eqid 
 |-  ( 0g ` ( Scalar ` m ) ) = ( 0g ` ( Scalar ` m ) )
6 1 2 3 4 5 isldepslvec2 
 |-  ( ( m e. LVec /\ s e. ~P ( Base ` m ) ) -> ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) <-> s linDepS m ) )
7 6 bicomd 
 |-  ( ( m e. LVec /\ s e. ~P ( Base ` m ) ) -> ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
8 7 rgen2 
 |-  A. m e. LVec A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
9 ldepsnlinc 
 |-  E. m e. LMod E. s e. ~P ( Base ` m ) ( s linDepS m /\ A. v e. s A. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) )
10 df-ne 
 |-  ( ( f ( linC ` m ) ( s \ { v } ) ) =/= v <-> -. ( f ( linC ` m ) ( s \ { v } ) ) = v )
11 10 imbi2i 
 |-  ( ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) <-> ( f finSupp ( 0g ` ( Scalar ` m ) ) -> -. ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
12 imnan 
 |-  ( ( f finSupp ( 0g ` ( Scalar ` m ) ) -> -. ( f ( linC ` m ) ( s \ { v } ) ) = v ) <-> -. ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
13 11 12 bitri 
 |-  ( ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) <-> -. ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
14 13 ralbii 
 |-  ( A. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) <-> A. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) -. ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
15 ralnex 
 |-  ( A. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) -. ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) <-> -. E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
16 14 15 bitri 
 |-  ( A. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) <-> -. E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
17 16 ralbii 
 |-  ( A. v e. s A. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) <-> A. v e. s -. E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
18 ralnex 
 |-  ( A. v e. s -. E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) <-> -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
19 17 18 bitri 
 |-  ( A. v e. s A. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) <-> -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
20 19 anbi2i 
 |-  ( ( s linDepS m /\ A. v e. s A. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) ) <-> ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
21 20 2rexbii 
 |-  ( E. m e. LMod E. s e. ~P ( Base ` m ) ( s linDepS m /\ A. v e. s A. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) ) <-> E. m e. LMod E. s e. ~P ( Base ` m ) ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
22 9 21 mpbi 
 |-  E. m e. LMod E. s e. ~P ( Base ` m ) ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
23 22 orci 
 |-  ( E. m e. LMod E. s e. ~P ( Base ` m ) ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ E. m e. LMod E. s e. ~P ( Base ` m ) ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) )
24 r19.43 
 |-  ( E. m e. LMod ( E. s e. ~P ( Base ` m ) ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ E. s e. ~P ( Base ` m ) ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) <-> ( E. m e. LMod E. s e. ~P ( Base ` m ) ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ E. m e. LMod E. s e. ~P ( Base ` m ) ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) )
25 23 24 mpbir 
 |-  E. m e. LMod ( E. s e. ~P ( Base ` m ) ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ E. s e. ~P ( Base ` m ) ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) )
26 r19.43 
 |-  ( E. s e. ~P ( Base ` m ) ( ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) <-> ( E. s e. ~P ( Base ` m ) ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ E. s e. ~P ( Base ` m ) ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) )
27 26 rexbii 
 |-  ( E. m e. LMod E. s e. ~P ( Base ` m ) ( ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) <-> E. m e. LMod ( E. s e. ~P ( Base ` m ) ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ E. s e. ~P ( Base ` m ) ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) )
28 25 27 mpbir 
 |-  E. m e. LMod E. s e. ~P ( Base ` m ) ( ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) )
29 xor 
 |-  ( -. ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) <-> ( ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) )
30 29 bicomi 
 |-  ( ( ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) <-> -. ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
31 30 rexbii 
 |-  ( E. s e. ~P ( Base ` m ) ( ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) <-> E. s e. ~P ( Base ` m ) -. ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
32 rexnal 
 |-  ( E. s e. ~P ( Base ` m ) -. ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) <-> -. A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
33 31 32 bitri 
 |-  ( E. s e. ~P ( Base ` m ) ( ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) <-> -. A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
34 33 rexbii 
 |-  ( E. m e. LMod E. s e. ~P ( Base ` m ) ( ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) <-> E. m e. LMod -. A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
35 rexnal 
 |-  ( E. m e. LMod -. A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) <-> -. A. m e. LMod A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
36 34 35 bitri 
 |-  ( E. m e. LMod E. s e. ~P ( Base ` m ) ( ( s linDepS m /\ -. E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) \/ ( E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) /\ -. s linDepS m ) ) <-> -. A. m e. LMod A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
37 28 36 mpbi 
 |-  -. A. m e. LMod A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) )
38 8 37 pm3.2i 
 |-  ( A. m e. LVec A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) /\ -. A. m e. LMod A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )