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	$⊢ Z = ℤ_{ring} freeLMod \{0, 1\}$
	zlmodzxzsub.m	$⊢ \underset{˙}{-} = -_{Z}$
Assertion	zlmodzxzsubm	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} \underset{˙}{-} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A⟩, ⟨1, C⟩\} +_{Z} (-1 \cdot_{Z} \{⟨0, B⟩, ⟨1, D⟩\})$

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	$⊢ Z = ℤ_{ring} freeLMod \{0, 1\}$
2		zlmodzxzsub.m	$⊢ \underset{˙}{-} = -_{Z}$
3	1	zlmodzxzlmod	$⊢ (Z \in LMod \land ℤ_{ring} = Scalar (Z))$
4	3	simpli	$⊢ Z \in LMod$
5	4	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to Z \in LMod$
6	1	zlmodzxzel	$⊢ (A \in ℤ \land C \in ℤ) \to \{⟨0, A⟩, ⟨1, C⟩\} \in {Base}_{Z}$
7	6	ad2ant2r	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} \in {Base}_{Z}$
8	1	zlmodzxzel	$⊢ (B \in ℤ \land D \in ℤ) \to \{⟨0, B⟩, ⟨1, D⟩\} \in {Base}_{Z}$
9	8	ad2ant2l	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, B⟩, ⟨1, D⟩\} \in {Base}_{Z}$
10		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
11		eqid	$⊢ +_{Z} = +_{Z}$
12	3	simpri	$⊢ ℤ_{ring} = Scalar (Z)$
13		eqid	$⊢ \cdot_{Z} = \cdot_{Z}$
14		eqid	$⊢ {inv}_{g} (ℤ_{ring}) = {inv}_{g} (ℤ_{ring})$
15		zring1	$⊢ 1 = 1_{ℤ_{ring}}$
16	10 11 2 12 13 14 15	lmodvsubval2	$⊢ (Z \in LMod \land \{⟨0, A⟩, ⟨1, C⟩\} \in {Base}_{Z} \land \{⟨0, B⟩, ⟨1, D⟩\} \in {Base}_{Z}) \to \{⟨0, A⟩, ⟨1, C⟩\} \underset{˙}{-} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A⟩, ⟨1, C⟩\} +_{Z} ({inv}_{g} (ℤ_{ring}) (1) \cdot_{Z} \{⟨0, B⟩, ⟨1, D⟩\})$
17	5 7 9 16	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} \underset{˙}{-} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A⟩, ⟨1, C⟩\} +_{Z} ({inv}_{g} (ℤ_{ring}) (1) \cdot_{Z} \{⟨0, B⟩, ⟨1, D⟩\})$
18		1z	$⊢ 1 \in ℤ$
19		zringinvg	$⊢ 1 \in ℤ \to - 1 = {inv}_{g} (ℤ_{ring}) (1)$
20	18 19	mp1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to - 1 = {inv}_{g} (ℤ_{ring}) (1)$
21	20	eqcomd	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to {inv}_{g} (ℤ_{ring}) (1) = - 1$
22	21	oveq1d	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to {inv}_{g} (ℤ_{ring}) (1) \cdot_{Z} \{⟨0, B⟩, ⟨1, D⟩\} = -1 \cdot_{Z} \{⟨0, B⟩, ⟨1, D⟩\}$
23	22	oveq2d	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} +_{Z} ({inv}_{g} (ℤ_{ring}) (1) \cdot_{Z} \{⟨0, B⟩, ⟨1, D⟩\}) = \{⟨0, A⟩, ⟨1, C⟩\} +_{Z} (-1 \cdot_{Z} \{⟨0, B⟩, ⟨1, D⟩\})$
24	17 23	eqtrd	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} \underset{˙}{-} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A⟩, ⟨1, C⟩\} +_{Z} (-1 \cdot_{Z} \{⟨0, B⟩, ⟨1, D⟩\})$

Metamath Proof Explorer

Theorem zlmodzxzsubm

Proof