Metamath Proof Explorer

Theorem zlmodzxzequap

Description: Example of an equation within the ZZ-module ZZ X. ZZ (see example in Roman p. 112 for a linearly dependent set), written as a sum. (Contributed by AV, 24-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 >. }
zlmodzxzequap.o 
|- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
zlmodzxzequap.m 
|- .+ = ( +g ` Z )
zlmodzxzequap.t 
|- .xb = ( .s ` Z )
Assertion zlmodzxzequap 
|- ( ( 2 .xb A ) .+ ( -u 3 .xb B ) ) = .0.

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 zlmodzxzequap.o 
 |-  .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
5 zlmodzxzequap.m 
 |-  .+ = ( +g ` Z )
6 zlmodzxzequap.t 
 |-  .xb = ( .s ` Z )
7 3cn 
 |-  3 e. CC
8 2cn 
 |-  2 e. CC
9 7 8 mulneg1i 
 |-  ( -u 3 x. 2 ) = -u ( 3 x. 2 )
10 9 oveq2i 
 |-  ( ( 2 x. 3 ) + ( -u 3 x. 2 ) ) = ( ( 2 x. 3 ) + -u ( 3 x. 2 ) )
11 8 7 mulcli 
 |-  ( 2 x. 3 ) e. CC
12 7 8 mulcli 
 |-  ( 3 x. 2 ) e. CC
13 negsub 
 |-  ( ( ( 2 x. 3 ) e. CC /\ ( 3 x. 2 ) e. CC ) -> ( ( 2 x. 3 ) + -u ( 3 x. 2 ) ) = ( ( 2 x. 3 ) - ( 3 x. 2 ) ) )
14 7 8 mulcomi 
 |-  ( 3 x. 2 ) = ( 2 x. 3 )
15 14 oveq2i 
 |-  ( ( 2 x. 3 ) - ( 3 x. 2 ) ) = ( ( 2 x. 3 ) - ( 2 x. 3 ) )
16 11 subidi 
 |-  ( ( 2 x. 3 ) - ( 2 x. 3 ) ) = 0
17 15 16 eqtri 
 |-  ( ( 2 x. 3 ) - ( 3 x. 2 ) ) = 0
18 13 17 eqtrdi 
 |-  ( ( ( 2 x. 3 ) e. CC /\ ( 3 x. 2 ) e. CC ) -> ( ( 2 x. 3 ) + -u ( 3 x. 2 ) ) = 0 )
19 11 12 18 mp2an 
 |-  ( ( 2 x. 3 ) + -u ( 3 x. 2 ) ) = 0
20 10 19 eqtri 
 |-  ( ( 2 x. 3 ) + ( -u 3 x. 2 ) ) = 0
21 20 opeq2i 
 |-  <. 0 , ( ( 2 x. 3 ) + ( -u 3 x. 2 ) ) >. = <. 0 , 0 >.
22 4cn 
 |-  4 e. CC
23 7 22 mulneg1i 
 |-  ( -u 3 x. 4 ) = -u ( 3 x. 4 )
24 23 oveq2i 
 |-  ( ( 2 x. 6 ) + ( -u 3 x. 4 ) ) = ( ( 2 x. 6 ) + -u ( 3 x. 4 ) )
25 6cn 
 |-  6 e. CC
26 8 25 mulcli 
 |-  ( 2 x. 6 ) e. CC
27 7 22 mulcli 
 |-  ( 3 x. 4 ) e. CC
28 26 27 negsubi 
 |-  ( ( 2 x. 6 ) + -u ( 3 x. 4 ) ) = ( ( 2 x. 6 ) - ( 3 x. 4 ) )
29 2t6m3t4e0 
 |-  ( ( 2 x. 6 ) - ( 3 x. 4 ) ) = 0
30 28 29 eqtri 
 |-  ( ( 2 x. 6 ) + -u ( 3 x. 4 ) ) = 0
31 24 30 eqtri 
 |-  ( ( 2 x. 6 ) + ( -u 3 x. 4 ) ) = 0
32 31 opeq2i 
 |-  <. 1 , ( ( 2 x. 6 ) + ( -u 3 x. 4 ) ) >. = <. 1 , 0 >.
33 21 32 preq12i 
 |-  { <. 0 , ( ( 2 x. 3 ) + ( -u 3 x. 2 ) ) >. , <. 1 , ( ( 2 x. 6 ) + ( -u 3 x. 4 ) ) >. } = { <. 0 , 0 >. , <. 1 , 0 >. }
34 2 oveq2i 
 |-  ( 2 .xb A ) = ( 2 .xb { <. 0 , 3 >. , <. 1 , 6 >. } )
35 2z 
 |-  2 e. ZZ
36 3z 
 |-  3 e. ZZ
37 6nn 
 |-  6 e. NN
38 37 nnzi 
 |-  6 e. ZZ
39 1 6 zlmodzxzscm 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ /\ 6 e. ZZ ) -> ( 2 .xb { <. 0 , 3 >. , <. 1 , 6 >. } ) = { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. } )
40 35 36 38 39 mp3an 
 |-  ( 2 .xb { <. 0 , 3 >. , <. 1 , 6 >. } ) = { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. }
41 34 40 eqtri 
 |-  ( 2 .xb A ) = { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. }
42 3 oveq2i 
 |-  ( -u 3 .xb B ) = ( -u 3 .xb { <. 0 , 2 >. , <. 1 , 4 >. } )
43 znegcl 
 |-  ( 3 e. ZZ -> -u 3 e. ZZ )
44 36 43 ax-mp 
 |-  -u 3 e. ZZ
45 4z 
 |-  4 e. ZZ
46 1 6 zlmodzxzscm 
 |-  ( ( -u 3 e. ZZ /\ 2 e. ZZ /\ 4 e. ZZ ) -> ( -u 3 .xb { <. 0 , 2 >. , <. 1 , 4 >. } ) = { <. 0 , ( -u 3 x. 2 ) >. , <. 1 , ( -u 3 x. 4 ) >. } )
47 44 35 45 46 mp3an 
 |-  ( -u 3 .xb { <. 0 , 2 >. , <. 1 , 4 >. } ) = { <. 0 , ( -u 3 x. 2 ) >. , <. 1 , ( -u 3 x. 4 ) >. }
48 42 47 eqtri 
 |-  ( -u 3 .xb B ) = { <. 0 , ( -u 3 x. 2 ) >. , <. 1 , ( -u 3 x. 4 ) >. }
49 41 48 oveq12i 
 |-  ( ( 2 .xb A ) .+ ( -u 3 .xb B ) ) = ( { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. } .+ { <. 0 , ( -u 3 x. 2 ) >. , <. 1 , ( -u 3 x. 4 ) >. } )
50 zmulcl 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ ) -> ( 2 x. 3 ) e. ZZ )
51 35 36 50 mp2an 
 |-  ( 2 x. 3 ) e. ZZ
52 zmulcl 
 |-  ( ( -u 3 e. ZZ /\ 2 e. ZZ ) -> ( -u 3 x. 2 ) e. ZZ )
53 44 35 52 mp2an 
 |-  ( -u 3 x. 2 ) e. ZZ
54 zmulcl 
 |-  ( ( 2 e. ZZ /\ 6 e. ZZ ) -> ( 2 x. 6 ) e. ZZ )
55 35 38 54 mp2an 
 |-  ( 2 x. 6 ) e. ZZ
56 zmulcl 
 |-  ( ( -u 3 e. ZZ /\ 4 e. ZZ ) -> ( -u 3 x. 4 ) e. ZZ )
57 44 45 56 mp2an 
 |-  ( -u 3 x. 4 ) e. ZZ
58 1 5 zlmodzxzadd 
 |-  ( ( ( ( 2 x. 3 ) e. ZZ /\ ( -u 3 x. 2 ) e. ZZ ) /\ ( ( 2 x. 6 ) e. ZZ /\ ( -u 3 x. 4 ) e. ZZ ) ) -> ( { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. } .+ { <. 0 , ( -u 3 x. 2 ) >. , <. 1 , ( -u 3 x. 4 ) >. } ) = { <. 0 , ( ( 2 x. 3 ) + ( -u 3 x. 2 ) ) >. , <. 1 , ( ( 2 x. 6 ) + ( -u 3 x. 4 ) ) >. } )
59 51 53 55 57 58 mp4an 
 |-  ( { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. } .+ { <. 0 , ( -u 3 x. 2 ) >. , <. 1 , ( -u 3 x. 4 ) >. } ) = { <. 0 , ( ( 2 x. 3 ) + ( -u 3 x. 2 ) ) >. , <. 1 , ( ( 2 x. 6 ) + ( -u 3 x. 4 ) ) >. }
60 49 59 eqtri 
 |-  ( ( 2 .xb A ) .+ ( -u 3 .xb B ) ) = { <. 0 , ( ( 2 x. 3 ) + ( -u 3 x. 2 ) ) >. , <. 1 , ( ( 2 x. 6 ) + ( -u 3 x. 4 ) ) >. }
61 33 60 4 3eqtr4i 
 |-  ( ( 2 .xb A ) .+ ( -u 3 .xb B ) ) = .0.