Metamath Proof Explorer

Theorem zlmodzxzequa

Description: Example of an equation within the ZZ-module ZZ X. ZZ (see example in Roman p. 112 for a linearly dependent set). (Contributed by AV, 22-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzequa.z 
|- Z = ( ZZring freeLMod { 0 , 1 } )
zlmodzxzequa.o 
|- .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
zlmodzxzequa.t 
|- .xb = ( .s ` Z )
zlmodzxzequa.m 
|- .- = ( -g ` Z )
zlmodzxzequa.a 
|- A = { <. 0 , 3 >. , <. 1 , 6 >. }
zlmodzxzequa.b 
|- B = { <. 0 , 2 >. , <. 1 , 4 >. }
Assertion zlmodzxzequa 
|- ( ( 2 .xb A ) .- ( 3 .xb B ) ) = .0.

Proof

Step Hyp Ref Expression
1 zlmodzxzequa.z 
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 zlmodzxzequa.o 
 |-  .0. = { <. 0 , 0 >. , <. 1 , 0 >. }
3 zlmodzxzequa.t 
 |-  .xb = ( .s ` Z )
4 zlmodzxzequa.m 
 |-  .- = ( -g ` Z )
5 zlmodzxzequa.a 
 |-  A = { <. 0 , 3 >. , <. 1 , 6 >. }
6 zlmodzxzequa.b 
 |-  B = { <. 0 , 2 >. , <. 1 , 4 >. }
7 3cn 
 |-  3 e. CC
8 7 2timesi 
 |-  ( 2 x. 3 ) = ( 3 + 3 )
9 3p3e6 
 |-  ( 3 + 3 ) = 6
10 8 9 eqtri 
 |-  ( 2 x. 3 ) = 6
11 3t2e6 
 |-  ( 3 x. 2 ) = 6
12 10 11 oveq12i 
 |-  ( ( 2 x. 3 ) - ( 3 x. 2 ) ) = ( 6 - 6 )
13 6cn 
 |-  6 e. CC
14 13 subidi 
 |-  ( 6 - 6 ) = 0
15 12 14 eqtri 
 |-  ( ( 2 x. 3 ) - ( 3 x. 2 ) ) = 0
16 15 opeq2i 
 |-  <. 0 , ( ( 2 x. 3 ) - ( 3 x. 2 ) ) >. = <. 0 , 0 >.
17 2t6m3t4e0 
 |-  ( ( 2 x. 6 ) - ( 3 x. 4 ) ) = 0
18 17 opeq2i 
 |-  <. 1 , ( ( 2 x. 6 ) - ( 3 x. 4 ) ) >. = <. 1 , 0 >.
19 16 18 preq12i 
 |-  { <. 0 , ( ( 2 x. 3 ) - ( 3 x. 2 ) ) >. , <. 1 , ( ( 2 x. 6 ) - ( 3 x. 4 ) ) >. } = { <. 0 , 0 >. , <. 1 , 0 >. }
20 5 oveq2i 
 |-  ( 2 .xb A ) = ( 2 .xb { <. 0 , 3 >. , <. 1 , 6 >. } )
21 2z 
 |-  2 e. ZZ
22 3z 
 |-  3 e. ZZ
23 6nn 
 |-  6 e. NN
24 23 nnzi 
 |-  6 e. ZZ
25 1 3 zlmodzxzscm 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ /\ 6 e. ZZ ) -> ( 2 .xb { <. 0 , 3 >. , <. 1 , 6 >. } ) = { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. } )
26 21 22 24 25 mp3an 
 |-  ( 2 .xb { <. 0 , 3 >. , <. 1 , 6 >. } ) = { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. }
27 20 26 eqtri 
 |-  ( 2 .xb A ) = { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. }
28 6 oveq2i 
 |-  ( 3 .xb B ) = ( 3 .xb { <. 0 , 2 >. , <. 1 , 4 >. } )
29 4z 
 |-  4 e. ZZ
30 1 3 zlmodzxzscm 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ /\ 4 e. ZZ ) -> ( 3 .xb { <. 0 , 2 >. , <. 1 , 4 >. } ) = { <. 0 , ( 3 x. 2 ) >. , <. 1 , ( 3 x. 4 ) >. } )
31 22 21 29 30 mp3an 
 |-  ( 3 .xb { <. 0 , 2 >. , <. 1 , 4 >. } ) = { <. 0 , ( 3 x. 2 ) >. , <. 1 , ( 3 x. 4 ) >. }
32 28 31 eqtri 
 |-  ( 3 .xb B ) = { <. 0 , ( 3 x. 2 ) >. , <. 1 , ( 3 x. 4 ) >. }
33 27 32 oveq12i 
 |-  ( ( 2 .xb A ) .- ( 3 .xb B ) ) = ( { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. } .- { <. 0 , ( 3 x. 2 ) >. , <. 1 , ( 3 x. 4 ) >. } )
34 zmulcl 
 |-  ( ( 2 e. ZZ /\ 3 e. ZZ ) -> ( 2 x. 3 ) e. ZZ )
35 21 22 34 mp2an 
 |-  ( 2 x. 3 ) e. ZZ
36 zmulcl 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ ) -> ( 3 x. 2 ) e. ZZ )
37 22 21 36 mp2an 
 |-  ( 3 x. 2 ) e. ZZ
38 zmulcl 
 |-  ( ( 2 e. ZZ /\ 6 e. ZZ ) -> ( 2 x. 6 ) e. ZZ )
39 21 24 38 mp2an 
 |-  ( 2 x. 6 ) e. ZZ
40 zmulcl 
 |-  ( ( 3 e. ZZ /\ 4 e. ZZ ) -> ( 3 x. 4 ) e. ZZ )
41 22 29 40 mp2an 
 |-  ( 3 x. 4 ) e. ZZ
42 1 4 zlmodzxzsub 
 |-  ( ( ( ( 2 x. 3 ) e. ZZ /\ ( 3 x. 2 ) e. ZZ ) /\ ( ( 2 x. 6 ) e. ZZ /\ ( 3 x. 4 ) e. ZZ ) ) -> ( { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. } .- { <. 0 , ( 3 x. 2 ) >. , <. 1 , ( 3 x. 4 ) >. } ) = { <. 0 , ( ( 2 x. 3 ) - ( 3 x. 2 ) ) >. , <. 1 , ( ( 2 x. 6 ) - ( 3 x. 4 ) ) >. } )
43 35 37 39 41 42 mp4an 
 |-  ( { <. 0 , ( 2 x. 3 ) >. , <. 1 , ( 2 x. 6 ) >. } .- { <. 0 , ( 3 x. 2 ) >. , <. 1 , ( 3 x. 4 ) >. } ) = { <. 0 , ( ( 2 x. 3 ) - ( 3 x. 2 ) ) >. , <. 1 , ( ( 2 x. 6 ) - ( 3 x. 4 ) ) >. }
44 33 43 eqtri 
 |-  ( ( 2 .xb A ) .- ( 3 .xb B ) ) = { <. 0 , ( ( 2 x. 3 ) - ( 3 x. 2 ) ) >. , <. 1 , ( ( 2 x. 6 ) - ( 3 x. 4 ) ) >. }
45 19 44 2 3eqtr4i 
 |-  ( ( 2 .xb A ) .- ( 3 .xb B ) ) = .0.