zlmodzxzadd

Description: The addition 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\}$
	zlmodzxzadd.p	$⊢ \underset{˙}{+} = +_{Z}$
Assertion	zlmodzxzadd	$⊢ ((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		zlmodzxzadd.p	$⊢ \underset{˙}{+} = +_{Z}$
3		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
4		zringring	$⊢ ℤ_{ring} \in Ring$
5	4	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to ℤ_{ring} \in Ring$
6		prex	$⊢ \{0, 1\} \in V$
7	6	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{0, 1\} \in V$
8		simpl	$⊢ (A \in ℤ \land B \in ℤ) \to A \in ℤ$
9		simpl	$⊢ (C \in ℤ \land D \in ℤ) \to C \in ℤ$
10	1	zlmodzxzel	$⊢ (A \in ℤ \land C \in ℤ) \to \{⟨0, A⟩, ⟨1, C⟩\} \in {Base}_{Z}$
11	8 9 10	syl2an	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} \in {Base}_{Z}$
12		simpr	$⊢ (A \in ℤ \land B \in ℤ) \to B \in ℤ$
13		simpr	$⊢ (C \in ℤ \land D \in ℤ) \to D \in ℤ$
14	1	zlmodzxzel	$⊢ (B \in ℤ \land D \in ℤ) \to \{⟨0, B⟩, ⟨1, D⟩\} \in {Base}_{Z}$
15	12 13 14	syl2an	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, B⟩, ⟨1, D⟩\} \in {Base}_{Z}$
16		eqid	$⊢ +_{ℤ_{ring}} = +_{ℤ_{ring}}$
17	1 3 5 7 11 15 16 2	frlmplusgval	$⊢ ((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⟩\} {+_{ℤ_{ring}}}_{f} \{⟨0, B⟩, ⟨1, D⟩\}$
18		c0ex	$⊢ 0 \in V$
19		1ex	$⊢ 1 \in V$
20	18 19	pm3.2i	$⊢ (0 \in V \land 1 \in V)$
21	20	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to (0 \in V \land 1 \in V)$
22	8 9	anim12i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to (A \in ℤ \land C \in ℤ)$
23		0ne1	$⊢ 0 \neq 1$
24	23	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to 0 \neq 1$
25		fnprg	$⊢ ((0 \in V \land 1 \in V) \land (A \in ℤ \land C \in ℤ) \land 0 \neq 1) \to \{⟨0, A⟩, ⟨1, C⟩\} Fn \{0, 1\}$
26	21 22 24 25	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} Fn \{0, 1\}$
27	12 13	anim12i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to (B \in ℤ \land D \in ℤ)$
28		fnprg	$⊢ ((0 \in V \land 1 \in V) \land (B \in ℤ \land D \in ℤ) \land 0 \neq 1) \to \{⟨0, B⟩, ⟨1, D⟩\} Fn \{0, 1\}$
29	21 27 24 28	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, B⟩, ⟨1, D⟩\} Fn \{0, 1\}$
30	7 26 29	offvalfv	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} {+_{ℤ_{ring}}}_{f} \{⟨0, B⟩, ⟨1, D⟩\} = (x \in \{0, 1\} ⟼ \{⟨0, A⟩, ⟨1, C⟩\} (x) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (x))$
31		zringplusg	$⊢ + = +_{ℤ_{ring}}$
32	31	eqcomi	$⊢ +_{ℤ_{ring}} = +$
33	32	oveqi	$⊢ A +_{ℤ_{ring}} B = A + B$
34	33	opeq2i	$⊢ ⟨0, A +_{ℤ_{ring}} B⟩ = ⟨0, A + B⟩$
35	32	oveqi	$⊢ C +_{ℤ_{ring}} D = C + D$
36	35	opeq2i	$⊢ ⟨1, C +_{ℤ_{ring}} D⟩ = ⟨1, C + D⟩$
37	34 36	preq12i	$⊢ \{⟨0, A +_{ℤ_{ring}} B⟩, ⟨1, C +_{ℤ_{ring}} D⟩\} = \{⟨0, A + B⟩, ⟨1, C + D⟩\}$
38	18	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to 0 \in V$
39	19	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to 1 \in V$
40		ovexd	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to A +_{ℤ_{ring}} B \in V$
41		ovexd	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to C +_{ℤ_{ring}} D \in V$
42		fveq2	$⊢ x = 0 \to \{⟨0, A⟩, ⟨1, C⟩\} (x) = \{⟨0, A⟩, ⟨1, C⟩\} (0)$
43		fveq2	$⊢ x = 0 \to \{⟨0, B⟩, ⟨1, D⟩\} (x) = \{⟨0, B⟩, ⟨1, D⟩\} (0)$
44	42 43	oveq12d	$⊢ x = 0 \to \{⟨0, A⟩, ⟨1, C⟩\} (x) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (x) = \{⟨0, A⟩, ⟨1, C⟩\} (0) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (0)$
45	8	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to A \in ℤ$
46		fvpr1g	$⊢ (0 \in V \land A \in ℤ \land 0 \neq 1) \to \{⟨0, A⟩, ⟨1, C⟩\} (0) = A$
47	38 45 24 46	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} (0) = A$
48	12	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to B \in ℤ$
49		fvpr1g	$⊢ (0 \in V \land B \in ℤ \land 0 \neq 1) \to \{⟨0, B⟩, ⟨1, D⟩\} (0) = B$
50	38 48 24 49	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, B⟩, ⟨1, D⟩\} (0) = B$
51	47 50	oveq12d	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} (0) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (0) = A +_{ℤ_{ring}} B$
52	44 51	sylan9eqr	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land x = 0) \to \{⟨0, A⟩, ⟨1, C⟩\} (x) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (x) = A +_{ℤ_{ring}} B$
53		fveq2	$⊢ x = 1 \to \{⟨0, A⟩, ⟨1, C⟩\} (x) = \{⟨0, A⟩, ⟨1, C⟩\} (1)$
54		fveq2	$⊢ x = 1 \to \{⟨0, B⟩, ⟨1, D⟩\} (x) = \{⟨0, B⟩, ⟨1, D⟩\} (1)$
55	53 54	oveq12d	$⊢ x = 1 \to \{⟨0, A⟩, ⟨1, C⟩\} (x) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (x) = \{⟨0, A⟩, ⟨1, C⟩\} (1) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (1)$
56	9	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to C \in ℤ$
57		fvpr2g	$⊢ (1 \in V \land C \in ℤ \land 0 \neq 1) \to \{⟨0, A⟩, ⟨1, C⟩\} (1) = C$
58	39 56 24 57	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} (1) = C$
59	13	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to D \in ℤ$
60		fvpr2g	$⊢ (1 \in V \land D \in ℤ \land 0 \neq 1) \to \{⟨0, B⟩, ⟨1, D⟩\} (1) = D$
61	39 59 24 60	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, B⟩, ⟨1, D⟩\} (1) = D$
62	58 61	oveq12d	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} (1) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (1) = C +_{ℤ_{ring}} D$
63	55 62	sylan9eqr	$⊢ (((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \land x = 1) \to \{⟨0, A⟩, ⟨1, C⟩\} (x) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (x) = C +_{ℤ_{ring}} D$
64	38 39 40 41 52 63	fmptpr	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A +_{ℤ_{ring}} B⟩, ⟨1, C +_{ℤ_{ring}} D⟩\} = (x \in \{0, 1\} ⟼ \{⟨0, A⟩, ⟨1, C⟩\} (x) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (x))$
65	37 64	syl5reqr	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to (x \in \{0, 1\} ⟼ \{⟨0, A⟩, ⟨1, C⟩\} (x) +_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, D⟩\} (x)) = \{⟨0, A + B⟩, ⟨1, C + D⟩\}$
66	17 30 65	3eqtrd	$⊢ ((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 zlmodzxzadd

Proof