Metamath Proof Explorer

Theorem zlmodzxzsubm

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

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

Proof

Step Hyp Ref Expression
1 zlmodzxz.z ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2 zlmodzxzsub.m ⊢ − = ( -g ‘ 𝑍 )
3 1 zlmodzxzlmod ⊢ ( 𝑍 ∈ LMod ∧ ℤring = ( Scalar ‘ 𝑍 ) )
4 3 simpli ⊢ 𝑍 ∈ LMod
5 4 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 𝑍 ∈ LMod )
6 1 zlmodzxzel ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) )
7 6 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) )
8 1 zlmodzxzel ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ∈ ( Base ‘ 𝑍 ) )
9 8 ad2ant2l ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ∈ ( Base ‘ 𝑍 ) )
10 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
11 eqid ⊢ ( +g ‘ 𝑍 ) = ( +g ‘ 𝑍 )
12 3 simpri ⊢ ℤring = ( Scalar ‘ 𝑍 )
13 eqid ⊢ ( ·𝑠 ‘ 𝑍 ) = ( ·𝑠 ‘ 𝑍 )
14 eqid ⊢ ( invg ‘ ℤring ) = ( invg ‘ ℤring )
15 zring1 ⊢ 1 = ( 1r ‘ ℤring )
16 10 11 2 12 13 14 15 lmodvsubval2 ⊢ ( ( 𝑍 ∈ LMod ∧ { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) ∧ { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ∈ ( Base ‘ 𝑍 ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } − { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ( +g ‘ 𝑍 ) ( ( ( invg ‘ ℤring ) ‘ 1 ) ( ·𝑠 ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) ) )
17 5 7 9 16 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } − { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ( +g ‘ 𝑍 ) ( ( ( invg ‘ ℤring ) ‘ 1 ) ( ·𝑠 ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) ) )
18 1z ⊢ 1 ∈ ℤ
19 zringinvg ⊢ ( 1 ∈ ℤ → - 1 = ( ( invg ‘ ℤring ) ‘ 1 ) )
20 18 19 mp1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → - 1 = ( ( invg ‘ ℤring ) ‘ 1 ) )
21 20 eqcomd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( invg ‘ ℤring ) ‘ 1 ) = - 1 )
22 21 oveq1d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( ( invg ‘ ℤring ) ‘ 1 ) ( ·𝑠 ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = ( - 1 ( ·𝑠 ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) )
23 22 oveq2d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ( +g ‘ 𝑍 ) ( ( ( invg ‘ ℤring ) ‘ 1 ) ( ·𝑠 ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ( +g ‘ 𝑍 ) ( - 1 ( ·𝑠 ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) ) )
24 17 23 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } − { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ( +g ‘ 𝑍 ) ( - 1 ( ·𝑠 ‘ 𝑍 ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) ) )