Metamath Proof Explorer

Theorem zlmodzxzsub

Description: The subtraction of the ZZ-module ZZ X. ZZ . (Contributed by AV, 22-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxz.z ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
zlmodzxzsub.m ⊢ − = ( -g ‘ 𝑍 )
Assertion zlmodzxzsub ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } − { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } )

Proof

Step Hyp Ref Expression
1 zlmodzxz.z ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2 zlmodzxzsub.m ⊢ − = ( -g ‘ 𝑍 )
3 zsubcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 − 𝐵 ) ∈ ℤ )
4 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℤ )
5 3 4 jca ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) )
6 zsubcl ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( 𝐶 − 𝐷 ) ∈ ℤ )
7 simpr ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → 𝐷 ∈ ℤ )
8 6 7 jca ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( 𝐶 − 𝐷 ) ∈ ℤ ∧ 𝐷 ∈ ℤ ) )
9 eqid ⊢ ( +g ‘ 𝑍 ) = ( +g ‘ 𝑍 )
10 1 9 zlmodzxzadd ⊢ ( ( ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐶 − 𝐷 ) ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ( +g ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , ( ( 𝐴 − 𝐵 ) + 𝐵 ) ⟩ , ⟨ 1 , ( ( 𝐶 − 𝐷 ) + 𝐷 ) ⟩ } )
11 5 8 10 syl2an ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ( +g ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , ( ( 𝐴 − 𝐵 ) + 𝐵 ) ⟩ , ⟨ 1 , ( ( 𝐶 − 𝐷 ) + 𝐷 ) ⟩ } )
12 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
13 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
14 npcan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐵 ) + 𝐵 ) = 𝐴 )
15 12 13 14 syl2an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 − 𝐵 ) + 𝐵 ) = 𝐴 )
16 15 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( 𝐴 − 𝐵 ) + 𝐵 ) = 𝐴 )
17 16 opeq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ⟨ 0 , ( ( 𝐴 − 𝐵 ) + 𝐵 ) ⟩ = ⟨ 0 , 𝐴 ⟩ )
18 zcn ⊢ ( 𝐶 ∈ ℤ → 𝐶 ∈ ℂ )
19 zcn ⊢ ( 𝐷 ∈ ℤ → 𝐷 ∈ ℂ )
20 npcan ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( 𝐶 − 𝐷 ) + 𝐷 ) = 𝐶 )
21 18 19 20 syl2an ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( 𝐶 − 𝐷 ) + 𝐷 ) = 𝐶 )
22 21 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( 𝐶 − 𝐷 ) + 𝐷 ) = 𝐶 )
23 22 opeq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ⟨ 1 , ( ( 𝐶 − 𝐷 ) + 𝐷 ) ⟩ = ⟨ 1 , 𝐶 ⟩ )
24 17 23 preq12d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , ( ( 𝐴 − 𝐵 ) + 𝐵 ) ⟩ , ⟨ 1 , ( ( 𝐶 − 𝐷 ) + 𝐷 ) ⟩ } = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } )
25 11 24 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ( +g ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } )
26 1 zlmodzxzlmod ⊢ ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) )
27 lmodgrp ⊢ ( 𝑍 ∈ LMod → 𝑍 ∈ Grp )
28 27 adantr ⊢ ( ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) ) → 𝑍 ∈ Grp )
29 26 28 mp1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 𝑍 ∈ Grp )
30 1 zlmodzxzel ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) )
31 30 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) )
32 1 zlmodzxzel ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ∈ ( Base ‘ 𝑍 ) )
33 4 7 32 syl2an ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ∈ ( Base ‘ 𝑍 ) )
34 1 zlmodzxzel ⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℤ ∧ ( 𝐶 − 𝐷 ) ∈ ℤ ) → { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ∈ ( Base ‘ 𝑍 ) )
35 3 6 34 syl2an ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ∈ ( Base ‘ 𝑍 ) )
36 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
37 36 9 2 grpsubadd ⊢ ( ( 𝑍 ∈ Grp ∧ ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) ∧ { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ∈ ( Base ‘ 𝑍 ) ∧ { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ∈ ( Base ‘ 𝑍 ) ) ) → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } − { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ↔ ( { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ( +g ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ) )
38 29 31 33 35 37 syl13anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } − { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ↔ ( { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } ( +g ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ) )
39 25 38 mpbird ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } − { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , ( 𝐴 − 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 − 𝐷 ) ⟩ } )