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	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
	zlmodzxzldep.a	⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
	zlmodzxzldep.b	⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
	zlmodzxzequap.o	⊢ 0 = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
	zlmodzxzequap.m	⊢ + = ( +g ‘ 𝑍 )
	zlmodzxzequap.t	⊢ ∙ = ( ·𝑠 ‘ 𝑍 )
Assertion	zlmodzxzequap	⊢ ( ( 2 ∙ 𝐴 ) + ( - 3 ∙ 𝐵 ) ) = 0

Proof

Step	Hyp	Ref	Expression
1		zlmodzxzldep.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2		zlmodzxzldep.a	⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
3		zlmodzxzldep.b	⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
4		zlmodzxzequap.o	⊢ 0 = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
5		zlmodzxzequap.m	⊢ + = ( +g ‘ 𝑍 )
6		zlmodzxzequap.t	⊢ ∙ = ( ·𝑠 ‘ 𝑍 )
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 ∙ 𝐴 ) = ( 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 ∙ 𝐴 ) = { ⟨ 0 , ( 2 · 3 ) ⟩ , ⟨ 1 , ( 2 · 6 ) ⟩ }
42	3	oveq2i	⊢ ( - 3 ∙ 𝐵 ) = ( - 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 ∙ 𝐵 ) = { ⟨ 0 , ( - 3 · 2 ) ⟩ , ⟨ 1 , ( - 3 · 4 ) ⟩ }
49	41 48	oveq12i	⊢ ( ( 2 ∙ 𝐴 ) + ( - 3 ∙ 𝐵 ) ) = ( { ⟨ 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 ∙ 𝐴 ) + ( - 3 ∙ 𝐵 ) ) = { ⟨ 0 , ( ( 2 · 3 ) + ( - 3 · 2 ) ) ⟩ , ⟨ 1 , ( ( 2 · 6 ) + ( - 3 · 4 ) ) ⟩ }
61	33 60 4	3eqtr4i	⊢ ( ( 2 ∙ 𝐴 ) + ( - 3 ∙ 𝐵 ) ) = 0