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	18	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to 0 \in V$
32	19	a1i	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to 1 \in V$
33		ovexd	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to A +_{ℤ_{ring}} B \in V$
34		ovexd	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to C +_{ℤ_{ring}} D \in V$
35		fveq2	$⊢ x = 0 \to \{⟨0, A⟩, ⟨1, C⟩\} (x) = \{⟨0, A⟩, ⟨1, C⟩\} (0)$
36		fveq2	$⊢ x = 0 \to \{⟨0, B⟩, ⟨1, D⟩\} (x) = \{⟨0, B⟩, ⟨1, D⟩\} (0)$
37	35 36	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)$
38	8	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to A \in ℤ$
39		fvpr1g	$⊢ (0 \in V \land A \in ℤ \land 0 \neq 1) \to \{⟨0, A⟩, ⟨1, C⟩\} (0) = A$
40	31 38 24 39	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} (0) = A$
41	12	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to B \in ℤ$
42		fvpr1g	$⊢ (0 \in V \land B \in ℤ \land 0 \neq 1) \to \{⟨0, B⟩, ⟨1, D⟩\} (0) = B$
43	31 41 24 42	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, B⟩, ⟨1, D⟩\} (0) = B$
44	40 43	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$
45	37 44	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$
46		fveq2	$⊢ x = 1 \to \{⟨0, A⟩, ⟨1, C⟩\} (x) = \{⟨0, A⟩, ⟨1, C⟩\} (1)$
47		fveq2	$⊢ x = 1 \to \{⟨0, B⟩, ⟨1, D⟩\} (x) = \{⟨0, B⟩, ⟨1, D⟩\} (1)$
48	46 47	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)$
49	9	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to C \in ℤ$
50		fvpr2g	$⊢ (1 \in V \land C \in ℤ \land 0 \neq 1) \to \{⟨0, A⟩, ⟨1, C⟩\} (1) = C$
51	32 49 24 50	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, A⟩, ⟨1, C⟩\} (1) = C$
52	13	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to D \in ℤ$
53		fvpr2g	$⊢ (1 \in V \land D \in ℤ \land 0 \neq 1) \to \{⟨0, B⟩, ⟨1, D⟩\} (1) = D$
54	32 52 24 53	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land (C \in ℤ \land D \in ℤ)) \to \{⟨0, B⟩, ⟨1, D⟩\} (1) = D$
55	51 54	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$
56	48 55	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$
57	31 32 33 34 45 56	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))$
58		zringplusg	$⊢ + = +_{ℤ_{ring}}$
59	58	eqcomi	$⊢ +_{ℤ_{ring}} = +$
60	59	oveqi	$⊢ A +_{ℤ_{ring}} B = A + B$
61	60	opeq2i	$⊢ ⟨0, A +_{ℤ_{ring}} B⟩ = ⟨0, A + B⟩$
62	59	oveqi	$⊢ C +_{ℤ_{ring}} D = C + D$
63	62	opeq2i	$⊢ ⟨1, C +_{ℤ_{ring}} D⟩ = ⟨1, C + D⟩$
64	61 63	preq12i	$⊢ \{⟨0, A +_{ℤ_{ring}} B⟩, ⟨1, C +_{ℤ_{ring}} D⟩\} = \{⟨0, A + B⟩, ⟨1, C + D⟩\}$
65	57 64	eqtr3di	$⊢ ((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