Metamath Proof Explorer

Theorem ldepsnlinc

Description: The reverse implication of islindeps2 does not hold for arbitrary (left) modules, see note in Roman p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combination of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa and zlmodzxznm . (Contributed by AV, 25-May-2019) (Revised by AV, 30-Jul-2019)

Ref Expression
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ZZring freeLMod { 0 , 1 } ) = ( ZZring freeLMod { 0 , 1 } )
2 1 zlmodzxzlmod 
 |-  ( ( ZZring freeLMod { 0 , 1 } ) e. LMod /\ ZZring = ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) )
3 2 simpli 
 |-  ( ZZring freeLMod { 0 , 1 } ) e. LMod
4 3z 
 |-  3 e. ZZ
5 6nn 
 |-  6 e. NN
6 5 nnzi 
 |-  6 e. ZZ
7 1 zlmodzxzel 
 |-  ( ( 3 e. ZZ /\ 6 e. ZZ ) -> { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) )
8 4 6 7 mp2an 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` ( ZZring freeLMod { 0 , 1 } ) )
9 2z 
 |-  2 e. ZZ
10 4z 
 |-  4 e. ZZ
11 1 zlmodzxzel 
 |-  ( ( 2 e. ZZ /\ 4 e. ZZ ) -> { <. 0 , 2 >. , <. 1 , 4 >. } e. ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) )
12 9 10 11 mp2an 
 |-  { <. 0 , 2 >. , <. 1 , 4 >. } e. ( Base ` ( ZZring freeLMod { 0 , 1 } ) )
13 prelpwi 
 |-  ( ( { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) /\ { <. 0 , 2 >. , <. 1 , 4 >. } e. ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } e. ~P ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) )
14 8 12 13 mp2an 
 |-  { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } e. ~P ( Base ` ( ZZring freeLMod { 0 , 1 } ) )
15 eqid 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } = { <. 0 , 3 >. , <. 1 , 6 >. }
16 eqid 
 |-  { <. 0 , 2 >. , <. 1 , 4 >. } = { <. 0 , 2 >. , <. 1 , 4 >. }
17 1 15 16 zlmodzxzldep 
 |-  { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } linDepS ( ZZring freeLMod { 0 , 1 } )
18 1 15 16 ldepsnlinclem1 
 |-  ( f e. ( ( Base ` ZZring ) ^m { { <. 0 , 2 >. , <. 1 , 4 >. } } ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 2 >. , <. 1 , 4 >. } } ) =/= { <. 0 , 3 >. , <. 1 , 6 >. } )
19 simpr 
 |-  ( ( ( ZZring freeLMod { 0 , 1 } ) e. LMod /\ ZZring = ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ZZring = ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) )
20 19 eqcomd 
 |-  ( ( ( ZZring freeLMod { 0 , 1 } ) e. LMod /\ ZZring = ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) = ZZring )
21 2 20 ax-mp 
 |-  ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) = ZZring
22 21 fveq2i 
 |-  ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) = ( Base ` ZZring )
23 22 oveq1i 
 |-  ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 2 >. , <. 1 , 4 >. } } ) = ( ( Base ` ZZring ) ^m { { <. 0 , 2 >. , <. 1 , 4 >. } } )
24 18 23 eleq2s 
 |-  ( f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 2 >. , <. 1 , 4 >. } } ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 2 >. , <. 1 , 4 >. } } ) =/= { <. 0 , 3 >. , <. 1 , 6 >. } )
25 24 a1d 
 |-  ( f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 2 >. , <. 1 , 4 >. } } ) -> ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 2 >. , <. 1 , 4 >. } } ) =/= { <. 0 , 3 >. , <. 1 , 6 >. } ) )
26 25 rgen 
 |-  A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 2 >. , <. 1 , 4 >. } } ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 2 >. , <. 1 , 4 >. } } ) =/= { <. 0 , 3 >. , <. 1 , 6 >. } )
27 1 15 16 ldepsnlinclem2 
 |-  ( f e. ( ( Base ` ZZring ) ^m { { <. 0 , 3 >. , <. 1 , 6 >. } } ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 3 >. , <. 1 , 6 >. } } ) =/= { <. 0 , 2 >. , <. 1 , 4 >. } )
28 22 oveq1i 
 |-  ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 3 >. , <. 1 , 6 >. } } ) = ( ( Base ` ZZring ) ^m { { <. 0 , 3 >. , <. 1 , 6 >. } } )
29 27 28 eleq2s 
 |-  ( f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 3 >. , <. 1 , 6 >. } } ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 3 >. , <. 1 , 6 >. } } ) =/= { <. 0 , 2 >. , <. 1 , 4 >. } )
30 29 a1d 
 |-  ( f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 3 >. , <. 1 , 6 >. } } ) -> ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 3 >. , <. 1 , 6 >. } } ) =/= { <. 0 , 2 >. , <. 1 , 4 >. } ) )
31 30 rgen 
 |-  A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 3 >. , <. 1 , 6 >. } } ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 3 >. , <. 1 , 6 >. } } ) =/= { <. 0 , 2 >. , <. 1 , 4 >. } )
32 prex 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } e. _V
33 prex 
 |-  { <. 0 , 2 >. , <. 1 , 4 >. } e. _V
34 sneq 
 |-  ( v = { <. 0 , 3 >. , <. 1 , 6 >. } -> { v } = { { <. 0 , 3 >. , <. 1 , 6 >. } } )
35 34 difeq2d 
 |-  ( v = { <. 0 , 3 >. , <. 1 , 6 >. } -> ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) = ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { { <. 0 , 3 >. , <. 1 , 6 >. } } ) )
36 1 15 16 zlmodzxzldeplem 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. }
37 difprsn1 
 |-  ( { <. 0 , 3 >. , <. 1 , 6 >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } -> ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { { <. 0 , 3 >. , <. 1 , 6 >. } } ) = { { <. 0 , 2 >. , <. 1 , 4 >. } } )
38 36 37 ax-mp 
 |-  ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { { <. 0 , 3 >. , <. 1 , 6 >. } } ) = { { <. 0 , 2 >. , <. 1 , 4 >. } }
39 35 38 eqtrdi 
 |-  ( v = { <. 0 , 3 >. , <. 1 , 6 >. } -> ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) = { { <. 0 , 2 >. , <. 1 , 4 >. } } )
40 39 oveq2d 
 |-  ( v = { <. 0 , 3 >. , <. 1 , 6 >. } -> ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) = ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 2 >. , <. 1 , 4 >. } } ) )
41 39 oveq2d 
 |-  ( v = { <. 0 , 3 >. , <. 1 , 6 >. } -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) = ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 2 >. , <. 1 , 4 >. } } ) )
42 id 
 |-  ( v = { <. 0 , 3 >. , <. 1 , 6 >. } -> v = { <. 0 , 3 >. , <. 1 , 6 >. } )
43 41 42 neeq12d 
 |-  ( v = { <. 0 , 3 >. , <. 1 , 6 >. } -> ( ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v <-> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 2 >. , <. 1 , 4 >. } } ) =/= { <. 0 , 3 >. , <. 1 , 6 >. } ) )
44 43 imbi2d 
 |-  ( v = { <. 0 , 3 >. , <. 1 , 6 >. } -> ( ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) <-> ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 2 >. , <. 1 , 4 >. } } ) =/= { <. 0 , 3 >. , <. 1 , 6 >. } ) ) )
45 40 44 raleqbidv 
 |-  ( v = { <. 0 , 3 >. , <. 1 , 6 >. } -> ( A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) <-> A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 2 >. , <. 1 , 4 >. } } ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 2 >. , <. 1 , 4 >. } } ) =/= { <. 0 , 3 >. , <. 1 , 6 >. } ) ) )
46 sneq 
 |-  ( v = { <. 0 , 2 >. , <. 1 , 4 >. } -> { v } = { { <. 0 , 2 >. , <. 1 , 4 >. } } )
47 46 difeq2d 
 |-  ( v = { <. 0 , 2 >. , <. 1 , 4 >. } -> ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) = ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { { <. 0 , 2 >. , <. 1 , 4 >. } } ) )
48 difprsn2 
 |-  ( { <. 0 , 3 >. , <. 1 , 6 >. } =/= { <. 0 , 2 >. , <. 1 , 4 >. } -> ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { { <. 0 , 2 >. , <. 1 , 4 >. } } ) = { { <. 0 , 3 >. , <. 1 , 6 >. } } )
49 36 48 ax-mp 
 |-  ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { { <. 0 , 2 >. , <. 1 , 4 >. } } ) = { { <. 0 , 3 >. , <. 1 , 6 >. } }
50 47 49 eqtrdi 
 |-  ( v = { <. 0 , 2 >. , <. 1 , 4 >. } -> ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) = { { <. 0 , 3 >. , <. 1 , 6 >. } } )
51 50 oveq2d 
 |-  ( v = { <. 0 , 2 >. , <. 1 , 4 >. } -> ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) = ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 3 >. , <. 1 , 6 >. } } ) )
52 50 oveq2d 
 |-  ( v = { <. 0 , 2 >. , <. 1 , 4 >. } -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) = ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 3 >. , <. 1 , 6 >. } } ) )
53 id 
 |-  ( v = { <. 0 , 2 >. , <. 1 , 4 >. } -> v = { <. 0 , 2 >. , <. 1 , 4 >. } )
54 52 53 neeq12d 
 |-  ( v = { <. 0 , 2 >. , <. 1 , 4 >. } -> ( ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v <-> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 3 >. , <. 1 , 6 >. } } ) =/= { <. 0 , 2 >. , <. 1 , 4 >. } ) )
55 54 imbi2d 
 |-  ( v = { <. 0 , 2 >. , <. 1 , 4 >. } -> ( ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) <-> ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 3 >. , <. 1 , 6 >. } } ) =/= { <. 0 , 2 >. , <. 1 , 4 >. } ) ) )
56 51 55 raleqbidv 
 |-  ( v = { <. 0 , 2 >. , <. 1 , 4 >. } -> ( A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) <-> A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 3 >. , <. 1 , 6 >. } } ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 3 >. , <. 1 , 6 >. } } ) =/= { <. 0 , 2 >. , <. 1 , 4 >. } ) ) )
57 32 33 45 56 ralpr 
 |-  ( A. v e. { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) <-> ( A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 2 >. , <. 1 , 4 >. } } ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 2 >. , <. 1 , 4 >. } } ) =/= { <. 0 , 3 >. , <. 1 , 6 >. } ) /\ A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m { { <. 0 , 3 >. , <. 1 , 6 >. } } ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) { { <. 0 , 3 >. , <. 1 , 6 >. } } ) =/= { <. 0 , 2 >. , <. 1 , 4 >. } ) ) )
58 26 31 57 mpbir2an 
 |-  A. v e. { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v )
59 17 58 pm3.2i 
 |-  ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } linDepS ( ZZring freeLMod { 0 , 1 } ) /\ A. v e. { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) )
60 breq1 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> ( s linDepS ( ZZring freeLMod { 0 , 1 } ) <-> { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } linDepS ( ZZring freeLMod { 0 , 1 } ) ) )
61 id 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } )
62 difeq1 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> ( s \ { v } ) = ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) )
63 62 oveq2d 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) = ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) )
64 62 oveq2d 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) = ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) )
65 64 neeq1d 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> ( ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v <-> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) )
66 65 imbi2d 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> ( ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) <-> ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) ) )
67 63 66 raleqbidv 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> ( A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) <-> A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) ) )
68 61 67 raleqbidv 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> ( A. v e. s A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) <-> A. v e. { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) ) )
69 60 68 anbi12d 
 |-  ( s = { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } -> ( ( s linDepS ( ZZring freeLMod { 0 , 1 } ) /\ A. v e. s A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) ) <-> ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } linDepS ( ZZring freeLMod { 0 , 1 } ) /\ A. v e. { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) ) ) )
70 69 rspcev 
 |-  ( ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } e. ~P ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) /\ ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } linDepS ( ZZring freeLMod { 0 , 1 } ) /\ A. v e. { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( { { <. 0 , 3 >. , <. 1 , 6 >. } , { <. 0 , 2 >. , <. 1 , 4 >. } } \ { v } ) ) =/= v ) ) ) -> E. s e. ~P ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) ( s linDepS ( ZZring freeLMod { 0 , 1 } ) /\ A. v e. s A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) ) )
71 14 59 70 mp2an 
 |-  E. s e. ~P ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) ( s linDepS ( ZZring freeLMod { 0 , 1 } ) /\ A. v e. s A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) )
72 fveq2 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( Base ` m ) = ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) )
73 72 pweqd 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ~P ( Base ` m ) = ~P ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) )
74 breq2 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( s linDepS m <-> s linDepS ( ZZring freeLMod { 0 , 1 } ) ) )
75 2fveq3 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( Base ` ( Scalar ` m ) ) = ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) )
76 75 oveq1d 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( ( Base ` ( Scalar ` m ) ) ^m ( s \ { v } ) ) = ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) )
77 2fveq3 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( 0g ` ( Scalar ` m ) ) = ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) )
78 77 breq2d 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( f finSupp ( 0g ` ( Scalar ` m ) ) <-> f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ) )
79 fveq2 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( linC ` m ) = ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) )
80 79 oveqd 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( f ( linC ` m ) ( s \ { v } ) ) = ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) )
81 80 neeq1d 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( ( f ( linC ` m ) ( s \ { v } ) ) =/= v <-> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) )
82 78 81 imbi12d 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( ( f finSupp ( 0g ` ( Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) <-> ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) ) )
83 76 82 raleqbidv 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( 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 ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) ) )
84 83 ralbidv 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( 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 A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) ) )
85 74 84 anbi12d 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( ( 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 ( ZZring freeLMod { 0 , 1 } ) /\ A. v e. s A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) ) ) )
86 73 85 rexeqbidv 
 |-  ( m = ( ZZring freeLMod { 0 , 1 } ) -> ( 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. s e. ~P ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) ( s linDepS ( ZZring freeLMod { 0 , 1 } ) /\ A. v e. s A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) ) ) )
87 86 rspcev 
 |-  ( ( ( ZZring freeLMod { 0 , 1 } ) e. LMod /\ E. s e. ~P ( Base ` ( ZZring freeLMod { 0 , 1 } ) ) ( s linDepS ( ZZring freeLMod { 0 , 1 } ) /\ A. v e. s A. f e. ( ( Base ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` ( Scalar ` ( ZZring freeLMod { 0 , 1 } ) ) ) -> ( f ( linC ` ( ZZring freeLMod { 0 , 1 } ) ) ( s \ { v } ) ) =/= v ) ) ) -> 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 ) ) )
88 3 71 87 mp2an 
 |-  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 ) )