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 = ring 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 + ˙ = + Z
zlmodzxzequap.t ˙ = Z
Assertion zlmodzxzequap 2 ˙ A + ˙ -3 ˙ B = 0 ˙

Proof

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