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={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
	zlmodzxzldep.a	$$⊢A=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
	zlmodzxzldep.b	$$⊢B=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
	zlmodzxzequap.o	$$⊢\underset{\dot{}}{0}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
	zlmodzxzequap.m	$$⊢\underset{\dot{}}{+}={+}_Z$$
	zlmodzxzequap.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Z$$
Assertion	zlmodzxzequap	$$⊢\left(2\underset{\dot{}}{\bullet }A\right)\underset{\dot{}}{+}\left(-3\underset{\dot{}}{\bullet }B\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		zlmodzxzldep.z	$$⊢Z={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
2		zlmodzxzldep.a	$$⊢A=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
3		zlmodzxzldep.b	$$⊢B=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
4		zlmodzxzequap.o	$$⊢\underset{\dot{}}{0}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
5		zlmodzxzequap.m	$$⊢\underset{\dot{}}{+}={+}_Z$$
6		zlmodzxzequap.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Z$$
7		3cn	$$⊢3\in ℂ$$
8		2cn	$$⊢2\in ℂ$$
9	7 8	mulneg1i	$$⊢-3\cdot 2=-3\cdot 2$$
10	9	oveq2i	$$⊢2\cdot 3+-3\cdot 2=2\cdot 3+\left(-3\cdot 2\right)$$
11	8 7	mulcli	$$⊢2\cdot 3\in ℂ$$
12	7 8	mulcli	$$⊢3\cdot 2\in ℂ$$
13		negsub	$$⊢\left(2\cdot 3\in ℂ\wedge 3\cdot 2\in ℂ\right)\to 2\cdot 3+\left(-3\cdot 2\right)=2\cdot 3-3\cdot 2$$
14	7 8	mulcomi	$$⊢3\cdot 2=2\cdot 3$$
15	14	oveq2i	$$⊢2\cdot 3-3\cdot 2=2\cdot 3-2\cdot 3$$
16	11	subidi	$$⊢2\cdot 3-2\cdot 3=0$$
17	15 16	eqtri	$$⊢2\cdot 3-3\cdot 2=0$$
18	13 17	eqtrdi	$$⊢\left(2\cdot 3\in ℂ\wedge 3\cdot 2\in ℂ\right)\to 2\cdot 3+\left(-3\cdot 2\right)=0$$
19	11 12 18	mp2an	$$⊢2\cdot 3+\left(-3\cdot 2\right)=0$$
20	10 19	eqtri	$$⊢2\cdot 3+-3\cdot 2=0$$
21	20	opeq2i	$$⊢⟨0,2\cdot 3+-3\cdot 2⟩=⟨0,0⟩$$
22		4cn	$$⊢4\in ℂ$$
23	7 22	mulneg1i	$$⊢-3\cdot 4=-3\cdot 4$$
24	23	oveq2i	$$⊢2\cdot 6+-3\cdot 4=2\cdot 6+\left(-3\cdot 4\right)$$
25		6cn	$$⊢6\in ℂ$$
26	8 25	mulcli	$$⊢2\cdot 6\in ℂ$$
27	7 22	mulcli	$$⊢3\cdot 4\in ℂ$$
28	26 27	negsubi	$$⊢2\cdot 6+\left(-3\cdot 4\right)=2\cdot 6-3\cdot 4$$
29		2t6m3t4e0	$$⊢2\cdot 6-3\cdot 4=0$$
30	28 29	eqtri	$$⊢2\cdot 6+\left(-3\cdot 4\right)=0$$
31	24 30	eqtri	$$⊢2\cdot 6+-3\cdot 4=0$$
32	31	opeq2i	$$⊢⟨1,2\cdot 6+-3\cdot 4⟩=⟨1,0⟩$$
33	21 32	preq12i	$$⊢\left\{⟨0,2\cdot 3+-3\cdot 2⟩,⟨1,2\cdot 6+-3\cdot 4⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
34	2	oveq2i	$$⊢2\underset{\dot{}}{\bullet }A=2\underset{\dot{}}{\bullet }\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
35		2z	$$⊢2\in \mathbb{Z}$$
36		3z	$$⊢3\in \mathbb{Z}$$
37		6nn	$$⊢6\in \mathbb{N}$$
38	37	nnzi	$$⊢6\in \mathbb{Z}$$
39	1 6	zlmodzxzscm	$$⊢\left(2\in \mathbb{Z}\wedge 3\in \mathbb{Z}\wedge 6\in \mathbb{Z}\right)\to 2\underset{\dot{}}{\bullet }\left\{⟨0,3⟩,⟨1,6⟩\right\}=\left\{⟨0,2\cdot 3⟩,⟨1,2\cdot 6⟩\right\}$$
40	35 36 38 39	mp3an	$$⊢2\underset{\dot{}}{\bullet }\left\{⟨0,3⟩,⟨1,6⟩\right\}=\left\{⟨0,2\cdot 3⟩,⟨1,2\cdot 6⟩\right\}$$
41	34 40	eqtri	$$⊢2\underset{\dot{}}{\bullet }A=\left\{⟨0,2\cdot 3⟩,⟨1,2\cdot 6⟩\right\}$$
42	3	oveq2i	$$⊢-3\underset{\dot{}}{\bullet }B=-3\underset{\dot{}}{\bullet }\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
43		znegcl	$$⊢3\in \mathbb{Z}\to -3\in \mathbb{Z}$$
44	36 43	ax-mp	$$⊢-3\in \mathbb{Z}$$
45		4z	$$⊢4\in \mathbb{Z}$$
46	1 6	zlmodzxzscm	$$⊢\left(-3\in \mathbb{Z}\wedge 2\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to -3\underset{\dot{}}{\bullet }\left\{⟨0,2⟩,⟨1,4⟩\right\}=\left\{⟨0,-3\cdot 2⟩,⟨1,-3\cdot 4⟩\right\}$$
47	44 35 45 46	mp3an	$$⊢-3\underset{\dot{}}{\bullet }\left\{⟨0,2⟩,⟨1,4⟩\right\}=\left\{⟨0,-3\cdot 2⟩,⟨1,-3\cdot 4⟩\right\}$$
48	42 47	eqtri	$$⊢-3\underset{\dot{}}{\bullet }B=\left\{⟨0,-3\cdot 2⟩,⟨1,-3\cdot 4⟩\right\}$$
49	41 48	oveq12i	$$⊢\left(2\underset{\dot{}}{\bullet }A\right)\underset{\dot{}}{+}\left(-3\underset{\dot{}}{\bullet }B\right)=\left\{⟨0,2\cdot 3⟩,⟨1,2\cdot 6⟩\right\}\underset{\dot{}}{+}\left\{⟨0,-3\cdot 2⟩,⟨1,-3\cdot 4⟩\right\}$$
50		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\to 2\cdot 3\in \mathbb{Z}$$
51	35 36 50	mp2an	$$⊢2\cdot 3\in \mathbb{Z}$$
52		zmulcl	$$⊢\left(-3\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to -3\cdot 2\in \mathbb{Z}$$
53	44 35 52	mp2an	$$⊢-3\cdot 2\in \mathbb{Z}$$
54		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge 6\in \mathbb{Z}\right)\to 2\cdot 6\in \mathbb{Z}$$
55	35 38 54	mp2an	$$⊢2\cdot 6\in \mathbb{Z}$$
56		zmulcl	$$⊢\left(-3\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to -3\cdot 4\in \mathbb{Z}$$
57	44 45 56	mp2an	$$⊢-3\cdot 4\in \mathbb{Z}$$
58	1 5	zlmodzxzadd	$$⊢\left(\left(2\cdot 3\in \mathbb{Z}\wedge -3\cdot 2\in \mathbb{Z}\right)\wedge \left(2\cdot 6\in \mathbb{Z}\wedge -3\cdot 4\in \mathbb{Z}\right)\right)\to \left\{⟨0,2\cdot 3⟩,⟨1,2\cdot 6⟩\right\}\underset{\dot{}}{+}\left\{⟨0,-3\cdot 2⟩,⟨1,-3\cdot 4⟩\right\}=\left\{⟨0,2\cdot 3+-3\cdot 2⟩,⟨1,2\cdot 6+-3\cdot 4⟩\right\}$$
59	51 53 55 57 58	mp4an	$$⊢\left\{⟨0,2\cdot 3⟩,⟨1,2\cdot 6⟩\right\}\underset{\dot{}}{+}\left\{⟨0,-3\cdot 2⟩,⟨1,-3\cdot 4⟩\right\}=\left\{⟨0,2\cdot 3+-3\cdot 2⟩,⟨1,2\cdot 6+-3\cdot 4⟩\right\}$$
60	49 59	eqtri	$$⊢\left(2\underset{\dot{}}{\bullet }A\right)\underset{\dot{}}{+}\left(-3\underset{\dot{}}{\bullet }B\right)=\left\{⟨0,2\cdot 3+-3\cdot 2⟩,⟨1,2\cdot 6+-3\cdot 4⟩\right\}$$
61	33 60 4	3eqtr4i	$$⊢\left(2\underset{\dot{}}{\bullet }A\right)\underset{\dot{}}{+}\left(-3\underset{\dot{}}{\bullet }B\right)=\underset{\dot{}}{0}$$