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

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	$⊢ Z = ℤ_{ring} freeLMod \{0, 1\}$
2		zlmodzxzsub.m	$⊢ \underset{˙}{-} = -_{Z}$
3		zsubcl	$⊢ (A \in ℤ \land B \in ℤ) \to A - B \in ℤ$
4		simpr	$⊢ (A \in ℤ \land B \in ℤ) \to B \in ℤ$
5	3 4	jca	$⊢ (A \in ℤ \land B \in ℤ) \to (A - B \in ℤ \land B \in ℤ)$
6		zsubcl	$⊢ (C \in ℤ \land D \in ℤ) \to C - D \in ℤ$
7		simpr	$⊢ (C \in ℤ \land D \in ℤ) \to D \in ℤ$
8	6 7	jca	$⊢ (C \in ℤ \land D \in ℤ) \to (C - D \in ℤ \land D \in ℤ)$
9		eqid	$⊢ +_{Z} = +_{Z}$
10	1 9	zlmodzxzadd	$⊢ ((A - B \in ℤ \land B \in ℤ) \land (C - D \in ℤ \land D \in ℤ)) \to \{⟨0, A - B⟩, ⟨1, C - D⟩\} +_{Z} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A - B + B⟩, ⟨1, C - D + D⟩\}$
11	5 8 10	syl2an	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A - B⟩, ⟨1, C - D⟩\} +_{Z} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A - B + B⟩, ⟨1, C - D + D⟩\}$
12		zcn	$⊢ A \in ℤ \to A \in ℂ$
13		zcn	$⊢ B \in ℤ \to B \in ℂ$
14		npcan	$⊢ (A \in ℂ \land B \in ℂ) \to A - B + B = A$
15	12 13 14	syl2an	$⊢ (A \in ℤ \land B \in ℤ) \to A - B + B = A$
16	15	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to A - B + B = A$
17	16	opeq2d	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to ⟨0, A - B + B⟩ = ⟨0, A⟩$
18		zcn	$⊢ C \in ℤ \to C \in ℂ$
19		zcn	$⊢ D \in ℤ \to D \in ℂ$
20		npcan	$⊢ (C \in ℂ \land D \in ℂ) \to C - D + D = C$
21	18 19 20	syl2an	$⊢ (C \in ℤ \land D \in ℤ) \to C - D + D = C$
22	21	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to C - D + D = C$
23	22	opeq2d	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to ⟨1, C - D + D⟩ = ⟨1, C⟩$
24	17 23	preq12d	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A - B + B⟩, ⟨1, C - D + D⟩\} = \{⟨0, A⟩, ⟨1, C⟩\}$
25	11 24	eqtrd	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A - B⟩, ⟨1, C - D⟩\} +_{Z} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A⟩, ⟨1, C⟩\}$
26	1	zlmodzxzlmod	$⊢ (Z \in LMod \land ℤ_{ring} = Scalar (Z))$
27		lmodgrp	$⊢ Z \in LMod \to Z \in Grp$
28	27	adantr	$⊢ (Z \in LMod \land ℤ_{ring} = Scalar (Z)) \to Z \in Grp$
29	26 28	mp1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to Z \in Grp$
30	1	zlmodzxzel	$⊢ (A \in ℤ \land C \in ℤ) \to \{⟨0, A⟩, ⟨1, C⟩\} \in {Base}_{Z}$
31	30	ad2ant2r	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} \in {Base}_{Z}$
32	1	zlmodzxzel	$⊢ (B \in ℤ \land D \in ℤ) \to \{⟨0, B⟩, ⟨1, D⟩\} \in {Base}_{Z}$
33	4 7 32	syl2an	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, B⟩, ⟨1, D⟩\} \in {Base}_{Z}$
34	1	zlmodzxzel	$⊢ (A - B \in ℤ \land C - D \in ℤ) \to \{⟨0, A - B⟩, ⟨1, C - D⟩\} \in {Base}_{Z}$
35	3 6 34	syl2an	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A - B⟩, ⟨1, C - D⟩\} \in {Base}_{Z}$
36		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
37	36 9 2	grpsubadd	$⊢ (Z \in Grp \land (\{⟨0, A⟩, ⟨1, C⟩\} \in {Base}_{Z} \land \{⟨0, B⟩, ⟨1, D⟩\} \in {Base}_{Z} \land \{⟨0, A - B⟩, ⟨1, C - D⟩\} \in {Base}_{Z})) \to (\{⟨0, A⟩, ⟨1, C⟩\} \underset{˙}{-} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A - B⟩, ⟨1, C - D⟩\} \leftrightarrow \{⟨0, A - B⟩, ⟨1, C - D⟩\} +_{Z} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A⟩, ⟨1, C⟩\})$
38	29 31 33 35 37	syl13anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to (\{⟨0, A⟩, ⟨1, C⟩\} \underset{˙}{-} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A - B⟩, ⟨1, C - D⟩\} \leftrightarrow \{⟨0, A - B⟩, ⟨1, C - D⟩\} +_{Z} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A⟩, ⟨1, C⟩\})$
39	25 38	mpbird	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} \underset{˙}{-} \{⟨0, B⟩, ⟨1, D⟩\} = \{⟨0, A - B⟩, ⟨1, C - D⟩\}$

Metamath Proof Explorer

Theorem zlmodzxzsub

Proof