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

Proof

Step Hyp Ref Expression
1 zlmodzxzequa.z ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2 zlmodzxzequa.o ⊢ 0 = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
3 zlmodzxzequa.t ⊢ ∙ = ( ·𝑠 ‘ 𝑍 )
4 zlmodzxzequa.m ⊢ − = ( -g ‘ 𝑍 )
5 zlmodzxzequa.a ⊢ 𝐴 = { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ }
6 zlmodzxzequa.b ⊢ 𝐵 = { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ }
7 3cn ⊢ 3 ∈ ℂ
8 7 2timesi ⊢ ( 2 · 3 ) = ( 3 + 3 )
9 3p3e6 ⊢ ( 3 + 3 ) = 6
10 8 9 eqtri ⊢ ( 2 · 3 ) = 6
11 3t2e6 ⊢ ( 3 · 2 ) = 6
12 10 11 oveq12i ⊢ ( ( 2 · 3 ) − ( 3 · 2 ) ) = ( 6 − 6 )
13 6cn ⊢ 6 ∈ ℂ
14 13 subidi ⊢ ( 6 − 6 ) = 0
15 12 14 eqtri ⊢ ( ( 2 · 3 ) − ( 3 · 2 ) ) = 0
16 15 opeq2i ⊢ ⟨ 0 , ( ( 2 · 3 ) − ( 3 · 2 ) ) ⟩ = ⟨ 0 , 0 ⟩
17 2t6m3t4e0 ⊢ ( ( 2 · 6 ) − ( 3 · 4 ) ) = 0
18 17 opeq2i ⊢ ⟨ 1 , ( ( 2 · 6 ) − ( 3 · 4 ) ) ⟩ = ⟨ 1 , 0 ⟩
19 16 18 preq12i ⊢ { ⟨ 0 , ( ( 2 · 3 ) − ( 3 · 2 ) ) ⟩ , ⟨ 1 , ( ( 2 · 6 ) − ( 3 · 4 ) ) ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
20 5 oveq2i ⊢ ( 2 ∙ 𝐴 ) = ( 2 ∙ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } )
21 2z ⊢ 2 ∈ ℤ
22 3z ⊢ 3 ∈ ℤ
23 6nn ⊢ 6 ∈ ℕ
24 23 nnzi ⊢ 6 ∈ ℤ
25 1 3 zlmodzxzscm ⊢ ( ( 2 ∈ ℤ ∧ 3 ∈ ℤ ∧ 6 ∈ ℤ ) → ( 2 ∙ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ) = { ⟨ 0 , ( 2 · 3 ) ⟩ , ⟨ 1 , ( 2 · 6 ) ⟩ } )
26 21 22 24 25 mp3an ⊢ ( 2 ∙ { ⟨ 0 , 3 ⟩ , ⟨ 1 , 6 ⟩ } ) = { ⟨ 0 , ( 2 · 3 ) ⟩ , ⟨ 1 , ( 2 · 6 ) ⟩ }
27 20 26 eqtri ⊢ ( 2 ∙ 𝐴 ) = { ⟨ 0 , ( 2 · 3 ) ⟩ , ⟨ 1 , ( 2 · 6 ) ⟩ }
28 6 oveq2i ⊢ ( 3 ∙ 𝐵 ) = ( 3 ∙ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } )
29 4z ⊢ 4 ∈ ℤ
30 1 3 zlmodzxzscm ⊢ ( ( 3 ∈ ℤ ∧ 2 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 3 ∙ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) = { ⟨ 0 , ( 3 · 2 ) ⟩ , ⟨ 1 , ( 3 · 4 ) ⟩ } )
31 22 21 29 30 mp3an ⊢ ( 3 ∙ { ⟨ 0 , 2 ⟩ , ⟨ 1 , 4 ⟩ } ) = { ⟨ 0 , ( 3 · 2 ) ⟩ , ⟨ 1 , ( 3 · 4 ) ⟩ }
32 28 31 eqtri ⊢ ( 3 ∙ 𝐵 ) = { ⟨ 0 , ( 3 · 2 ) ⟩ , ⟨ 1 , ( 3 · 4 ) ⟩ }
33 27 32 oveq12i ⊢ ( ( 2 ∙ 𝐴 ) − ( 3 ∙ 𝐵 ) ) = ( { ⟨ 0 , ( 2 · 3 ) ⟩ , ⟨ 1 , ( 2 · 6 ) ⟩ } − { ⟨ 0 , ( 3 · 2 ) ⟩ , ⟨ 1 , ( 3 · 4 ) ⟩ } )
34 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 3 ∈ ℤ ) → ( 2 · 3 ) ∈ ℤ )
35 21 22 34 mp2an ⊢ ( 2 · 3 ) ∈ ℤ
36 zmulcl ⊢ ( ( 3 ∈ ℤ ∧ 2 ∈ ℤ ) → ( 3 · 2 ) ∈ ℤ )
37 22 21 36 mp2an ⊢ ( 3 · 2 ) ∈ ℤ
38 zmulcl ⊢ ( ( 2 ∈ ℤ ∧ 6 ∈ ℤ ) → ( 2 · 6 ) ∈ ℤ )
39 21 24 38 mp2an ⊢ ( 2 · 6 ) ∈ ℤ
40 zmulcl ⊢ ( ( 3 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 3 · 4 ) ∈ ℤ )
41 22 29 40 mp2an ⊢ ( 3 · 4 ) ∈ ℤ
42 1 4 zlmodzxzsub ⊢ ( ( ( ( 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 ) ) ⟩ } )
43 35 37 39 41 42 mp4an ⊢ ( { ⟨ 0 , ( 2 · 3 ) ⟩ , ⟨ 1 , ( 2 · 6 ) ⟩ } − { ⟨ 0 , ( 3 · 2 ) ⟩ , ⟨ 1 , ( 3 · 4 ) ⟩ } ) = { ⟨ 0 , ( ( 2 · 3 ) − ( 3 · 2 ) ) ⟩ , ⟨ 1 , ( ( 2 · 6 ) − ( 3 · 4 ) ) ⟩ }
44 33 43 eqtri ⊢ ( ( 2 ∙ 𝐴 ) − ( 3 ∙ 𝐵 ) ) = { ⟨ 0 , ( ( 2 · 3 ) − ( 3 · 2 ) ) ⟩ , ⟨ 1 , ( ( 2 · 6 ) − ( 3 · 4 ) ) ⟩ }
45 19 44 2 3eqtr4i ⊢ ( ( 2 ∙ 𝐴 ) − ( 3 ∙ 𝐵 ) ) = 0