Metamath Proof Explorer

Theorem zlmodzxzldep

Description: { A , B } is a linearly dependent set within the ZZ-module ZZ X. ZZ (see example in Roman p. 112). (Contributed by AV, 22-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzldep.z 
|- Z = ( ZZring freeLMod { 0 , 1 } )
zlmodzxzldep.a 
|- A = { <. 0 , 3 >. , <. 1 , 6 >. }
zlmodzxzldep.b 
|- B = { <. 0 , 2 >. , <. 1 , 4 >. }
Assertion zlmodzxzldep 
|- { A , B } linDepS Z

Proof

Step Hyp Ref Expression
1 zlmodzxzldep.z 
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 zlmodzxzldep.a 
 |-  A = { <. 0 , 3 >. , <. 1 , 6 >. }
3 zlmodzxzldep.b 
 |-  B = { <. 0 , 2 >. , <. 1 , 4 >. }
4 eqid 
 |-  { <. A , 2 >. , <. B , -u 3 >. } = { <. A , 2 >. , <. B , -u 3 >. }
5 1 2 3 4 zlmodzxzldeplem1 
 |-  { <. A , 2 >. , <. B , -u 3 >. } e. ( ZZ ^m { A , B } )
6 1 2 3 4 zlmodzxzldeplem2 
 |-  { <. A , 2 >. , <. B , -u 3 >. } finSupp 0
7 1 2 3 4 zlmodzxzldeplem3 
 |-  ( { <. A , 2 >. , <. B , -u 3 >. } ( linC ` Z ) { A , B } ) = ( 0g ` Z )
8 1 2 3 4 zlmodzxzldeplem4 
 |-  E. y e. { A , B } ( { <. A , 2 >. , <. B , -u 3 >. } ` y ) =/= 0
9 6 7 8 3pm3.2i 
 |-  ( { <. A , 2 >. , <. B , -u 3 >. } finSupp 0 /\ ( { <. A , 2 >. , <. B , -u 3 >. } ( linC ` Z ) { A , B } ) = ( 0g ` Z ) /\ E. y e. { A , B } ( { <. A , 2 >. , <. B , -u 3 >. } ` y ) =/= 0 )
10 breq1 
 |-  ( x = { <. A , 2 >. , <. B , -u 3 >. } -> ( x finSupp 0 <-> { <. A , 2 >. , <. B , -u 3 >. } finSupp 0 ) )
11 oveq1 
 |-  ( x = { <. A , 2 >. , <. B , -u 3 >. } -> ( x ( linC ` Z ) { A , B } ) = ( { <. A , 2 >. , <. B , -u 3 >. } ( linC ` Z ) { A , B } ) )
12 11 eqeq1d 
 |-  ( x = { <. A , 2 >. , <. B , -u 3 >. } -> ( ( x ( linC ` Z ) { A , B } ) = ( 0g ` Z ) <-> ( { <. A , 2 >. , <. B , -u 3 >. } ( linC ` Z ) { A , B } ) = ( 0g ` Z ) ) )
13 fveq1 
 |-  ( x = { <. A , 2 >. , <. B , -u 3 >. } -> ( x ` y ) = ( { <. A , 2 >. , <. B , -u 3 >. } ` y ) )
14 13 neeq1d 
 |-  ( x = { <. A , 2 >. , <. B , -u 3 >. } -> ( ( x ` y ) =/= 0 <-> ( { <. A , 2 >. , <. B , -u 3 >. } ` y ) =/= 0 ) )
15 14 rexbidv 
 |-  ( x = { <. A , 2 >. , <. B , -u 3 >. } -> ( E. y e. { A , B } ( x ` y ) =/= 0 <-> E. y e. { A , B } ( { <. A , 2 >. , <. B , -u 3 >. } ` y ) =/= 0 ) )
16 10 12 15 3anbi123d 
 |-  ( x = { <. A , 2 >. , <. B , -u 3 >. } -> ( ( x finSupp 0 /\ ( x ( linC ` Z ) { A , B } ) = ( 0g ` Z ) /\ E. y e. { A , B } ( x ` y ) =/= 0 ) <-> ( { <. A , 2 >. , <. B , -u 3 >. } finSupp 0 /\ ( { <. A , 2 >. , <. B , -u 3 >. } ( linC ` Z ) { A , B } ) = ( 0g ` Z ) /\ E. y e. { A , B } ( { <. A , 2 >. , <. B , -u 3 >. } ` y ) =/= 0 ) ) )
17 16 rspcev 
 |-  ( ( { <. A , 2 >. , <. B , -u 3 >. } e. ( ZZ ^m { A , B } ) /\ ( { <. A , 2 >. , <. B , -u 3 >. } finSupp 0 /\ ( { <. A , 2 >. , <. B , -u 3 >. } ( linC ` Z ) { A , B } ) = ( 0g ` Z ) /\ E. y e. { A , B } ( { <. A , 2 >. , <. B , -u 3 >. } ` y ) =/= 0 ) ) -> E. x e. ( ZZ ^m { A , B } ) ( x finSupp 0 /\ ( x ( linC ` Z ) { A , B } ) = ( 0g ` Z ) /\ E. y e. { A , B } ( x ` y ) =/= 0 ) )
18 5 9 17 mp2an 
 |-  E. x e. ( ZZ ^m { A , B } ) ( x finSupp 0 /\ ( x ( linC ` Z ) { A , B } ) = ( 0g ` Z ) /\ E. y e. { A , B } ( x ` y ) =/= 0 )
19 ovex 
 |-  ( ZZring freeLMod { 0 , 1 } ) e. _V
20 1 19 eqeltri 
 |-  Z e. _V
21 3z 
 |-  3 e. ZZ
22 6nn 
 |-  6 e. NN
23 22 nnzi 
 |-  6 e. ZZ
24 1 zlmodzxzel 
 |-  ( ( 3 e. ZZ /\ 6 e. ZZ ) -> { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` Z ) )
25 21 23 24 mp2an 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` Z )
26 2 25 eqeltri 
 |-  A e. ( Base ` Z )
27 2z 
 |-  2 e. ZZ
28 4z 
 |-  4 e. ZZ
29 1 zlmodzxzel 
 |-  ( ( 2 e. ZZ /\ 4 e. ZZ ) -> { <. 0 , 2 >. , <. 1 , 4 >. } e. ( Base ` Z ) )
30 27 28 29 mp2an 
 |-  { <. 0 , 2 >. , <. 1 , 4 >. } e. ( Base ` Z )
31 3 30 eqeltri 
 |-  B e. ( Base ` Z )
32 prelpwi 
 |-  ( ( A e. ( Base ` Z ) /\ B e. ( Base ` Z ) ) -> { A , B } e. ~P ( Base ` Z ) )
33 26 31 32 mp2an 
 |-  { A , B } e. ~P ( Base ` Z )
34 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
35 eqid 
 |-  ( 0g ` Z ) = ( 0g ` Z )
36 1 zlmodzxzlmod 
 |-  ( Z e. LMod /\ ZZring = ( Scalar ` Z ) )
37 36 simpri 
 |-  ZZring = ( Scalar ` Z )
38 zringbas 
 |-  ZZ = ( Base ` ZZring )
39 zring0 
 |-  0 = ( 0g ` ZZring )
40 34 35 37 38 39 islindeps 
 |-  ( ( Z e. _V /\ { A , B } e. ~P ( Base ` Z ) ) -> ( { A , B } linDepS Z <-> E. x e. ( ZZ ^m { A , B } ) ( x finSupp 0 /\ ( x ( linC ` Z ) { A , B } ) = ( 0g ` Z ) /\ E. y e. { A , B } ( x ` y ) =/= 0 ) ) )
41 20 33 40 mp2an 
 |-  ( { A , B } linDepS Z <-> E. x e. ( ZZ ^m { A , B } ) ( x finSupp 0 /\ ( x ( linC ` Z ) { A , B } ) = ( 0g ` Z ) /\ E. y e. { A , B } ( x ` y ) =/= 0 ) )
42 18 41 mpbir 
 |-  { A , B } linDepS Z