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=ringfreeLMod01
zlmodzxzequa.o 0˙=0010
zlmodzxzequa.t ˙=Z
zlmodzxzequa.m -˙=-Z
zlmodzxzequa.a A=0316
zlmodzxzequa.b B=0214
Assertion zlmodzxzequa 2˙A-˙3˙B=0˙

Proof

Step Hyp Ref Expression
1 zlmodzxzequa.z Z=ringfreeLMod01
2 zlmodzxzequa.o 0˙=0010
3 zlmodzxzequa.t ˙=Z
4 zlmodzxzequa.m -˙=-Z
5 zlmodzxzequa.a A=0316
6 zlmodzxzequa.b B=0214
7 3cn 3
8 7 2timesi 23=3+3
9 3p3e6 3+3=6
10 8 9 eqtri 23=6
11 3t2e6 32=6
12 10 11 oveq12i 2332=66
13 6cn 6
14 13 subidi 66=0
15 12 14 eqtri 2332=0
16 15 opeq2i 02332=00
17 2t6m3t4e0 2634=0
18 17 opeq2i 12634=10
19 16 18 preq12i 0233212634=0010
20 5 oveq2i 2˙A=2˙0316
21 2z 2
22 3z 3
23 6nn 6
24 23 nnzi 6
25 1 3 zlmodzxzscm 2362˙0316=023126
26 21 22 24 25 mp3an 2˙0316=023126
27 20 26 eqtri 2˙A=023126
28 6 oveq2i 3˙B=3˙0214
29 4z 4
30 1 3 zlmodzxzscm 3243˙0214=032134
31 22 21 29 30 mp3an 3˙0214=032134
32 28 31 eqtri 3˙B=032134
33 27 32 oveq12i 2˙A-˙3˙B=023126-˙032134
34 zmulcl 2323
35 21 22 34 mp2an 23
36 zmulcl 3232
37 22 21 36 mp2an 32
38 zmulcl 2626
39 21 24 38 mp2an 26
40 zmulcl 3434
41 22 29 40 mp2an 34
42 1 4 zlmodzxzsub 23322634023126-˙032134=0233212634
43 35 37 39 41 42 mp4an 023126-˙032134=0233212634
44 33 43 eqtri 2˙A-˙3˙B=0233212634
45 19 44 2 3eqtr4i 2˙A-˙3˙B=0˙