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={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
	zlmodzxzequa.o	$$⊢\underset{\dot{}}{0}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
	zlmodzxzequa.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Z$$
	zlmodzxzequa.m	$$⊢\underset{\dot{}}{-}={-}_Z$$
	zlmodzxzequa.a	$$⊢A=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
	zlmodzxzequa.b	$$⊢B=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
Assertion	zlmodzxzequa	$$⊢\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		zlmodzxzequa.z	$$⊢Z={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
2		zlmodzxzequa.o	$$⊢\underset{\dot{}}{0}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
3		zlmodzxzequa.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_Z$$
4		zlmodzxzequa.m	$$⊢\underset{\dot{}}{-}={-}_Z$$
5		zlmodzxzequa.a	$$⊢A=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
6		zlmodzxzequa.b	$$⊢B=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
7		3cn	$$⊢3\in ℂ$$
8	7	2timesi	$$⊢2\cdot 3=3+3$$
9		3p3e6	$$⊢3+3=6$$
10	8 9	eqtri	$$⊢2\cdot 3=6$$
11		3t2e6	$$⊢3\cdot 2=6$$
12	10 11	oveq12i	$$⊢2\cdot 3-3\cdot 2=6-6$$
13		6cn	$$⊢6\in ℂ$$
14	13	subidi	$$⊢6-6=0$$
15	12 14	eqtri	$$⊢2\cdot 3-3\cdot 2=0$$
16	15	opeq2i	$$⊢⟨0,2\cdot 3-3\cdot 2⟩=⟨0,0⟩$$
17		2t6m3t4e0	$$⊢2\cdot 6-3\cdot 4=0$$
18	17	opeq2i	$$⊢⟨1,2\cdot 6-3\cdot 4⟩=⟨1,0⟩$$
19	16 18	preq12i	$$⊢\left\{⟨0,2\cdot 3-3\cdot 2⟩,⟨1,2\cdot 6-3\cdot 4⟩\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
20	5	oveq2i	$$⊢2\underset{\dot{}}{\bullet }A=2\underset{\dot{}}{\bullet }\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
21		2z	$$⊢2\in \mathbb{Z}$$
22		3z	$$⊢3\in \mathbb{Z}$$
23		6nn	$$⊢6\in \mathbb{N}$$
24	23	nnzi	$$⊢6\in \mathbb{Z}$$
25	1 3	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\}$$
26	21 22 24 25	mp3an	$$⊢2\underset{\dot{}}{\bullet }\left\{⟨0,3⟩,⟨1,6⟩\right\}=\left\{⟨0,2\cdot 3⟩,⟨1,2\cdot 6⟩\right\}$$
27	20 26	eqtri	$$⊢2\underset{\dot{}}{\bullet }A=\left\{⟨0,2\cdot 3⟩,⟨1,2\cdot 6⟩\right\}$$
28	6	oveq2i	$$⊢3\underset{\dot{}}{\bullet }B=3\underset{\dot{}}{\bullet }\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
29		4z	$$⊢4\in \mathbb{Z}$$
30	1 3	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\}$$
31	22 21 29 30	mp3an	$$⊢3\underset{\dot{}}{\bullet }\left\{⟨0,2⟩,⟨1,4⟩\right\}=\left\{⟨0,3\cdot 2⟩,⟨1,3\cdot 4⟩\right\}$$
32	28 31	eqtri	$$⊢3\underset{\dot{}}{\bullet }B=\left\{⟨0,3\cdot 2⟩,⟨1,3\cdot 4⟩\right\}$$
33	27 32	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\}$$
34		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge 3\in \mathbb{Z}\right)\to 2\cdot 3\in \mathbb{Z}$$
35	21 22 34	mp2an	$$⊢2\cdot 3\in \mathbb{Z}$$
36		zmulcl	$$⊢\left(3\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to 3\cdot 2\in \mathbb{Z}$$
37	22 21 36	mp2an	$$⊢3\cdot 2\in \mathbb{Z}$$
38		zmulcl	$$⊢\left(2\in \mathbb{Z}\wedge 6\in \mathbb{Z}\right)\to 2\cdot 6\in \mathbb{Z}$$
39	21 24 38	mp2an	$$⊢2\cdot 6\in \mathbb{Z}$$
40		zmulcl	$$⊢\left(3\in \mathbb{Z}\wedge 4\in \mathbb{Z}\right)\to 3\cdot 4\in \mathbb{Z}$$
41	22 29 40	mp2an	$$⊢3\cdot 4\in \mathbb{Z}$$
42	1 4	zlmodzxzsub	$$⊢\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\}$$
43	35 37 39 41 42	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\}$$
44	33 43	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\}$$
45	19 44 2	3eqtr4i	$$⊢\left(2\underset{\dot{}}{\bullet }A\right)\underset{\dot{}}{-}\left(3\underset{\dot{}}{\bullet }B\right)=\underset{\dot{}}{0}$$