zlmodzxzscm

Description: The scalar multiplication of the ZZ-module ZZ X. ZZ . (Contributed by AV, 20-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypotheses	zlmodzxz.z	$⊢ Z = ℤ_{ring} freeLMod \{0, 1\}$
	zlmodzxzscm.t	$⊢ \underset{˙}{∙} = \cdot_{Z}$
Assertion	zlmodzxzscm	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \underset{˙}{∙} \{⟨0, B⟩, ⟨1, C⟩\} = \{⟨0, A B⟩, ⟨1, A C⟩\}$

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	$⊢ Z = ℤ_{ring} freeLMod \{0, 1\}$
2		zlmodzxzscm.t	$⊢ \underset{˙}{∙} = \cdot_{Z}$
3		prex	$⊢ \{0, 1\} \in V$
4	3	a1i	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to \{0, 1\} \in V$
5		fnconstg	$⊢ A \in ℤ \to (\{0, 1\} \times \{A\}) Fn \{0, 1\}$
6	5	3ad2ant1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (\{0, 1\} \times \{A\}) Fn \{0, 1\}$
7		c0ex	$⊢ 0 \in V$
8		1ex	$⊢ 1 \in V$
9	7 8	pm3.2i	$⊢ (0 \in V \land 1 \in V)$
10	9	a1i	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (0 \in V \land 1 \in V)$
11		3simpc	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (B \in ℤ \land C \in ℤ)$
12		0ne1	$⊢ 0 \neq 1$
13	12	a1i	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to 0 \neq 1$
14		fnprg	$⊢ ((0 \in V \land 1 \in V) \land (B \in ℤ \land C \in ℤ) \land 0 \neq 1) \to \{⟨0, B⟩, ⟨1, C⟩\} Fn \{0, 1\}$
15	10 11 13 14	syl3anc	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to \{⟨0, B⟩, ⟨1, C⟩\} Fn \{0, 1\}$
16	4 6 15	offvalfv	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (\{0, 1\} \times \{A\}) {\cdot_{ℤ_{ring}}}_{f} \{⟨0, B⟩, ⟨1, C⟩\} = (x \in \{0, 1\} ⟼ (\{0, 1\} \times \{A\}) (x) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (x))$
17		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
18		eqid	$⊢ {Base}_{ℤ_{ring}} = {Base}_{ℤ_{ring}}$
19		simp1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \in ℤ$
20		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
21	19 20	eleqtrdi	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \in {Base}_{ℤ_{ring}}$
22	1	zlmodzxzel	$⊢ (B \in ℤ \land C \in ℤ) \to \{⟨0, B⟩, ⟨1, C⟩\} \in {Base}_{Z}$
23	22	3adant1	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to \{⟨0, B⟩, ⟨1, C⟩\} \in {Base}_{Z}$
24		eqid	$⊢ \cdot_{ℤ_{ring}} = \cdot_{ℤ_{ring}}$
25	1 17 18 4 21 23 2 24	frlmvscafval	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \underset{˙}{∙} \{⟨0, B⟩, ⟨1, C⟩\} = (\{0, 1\} \times \{A\}) {\cdot_{ℤ_{ring}}}_{f} \{⟨0, B⟩, ⟨1, C⟩\}$
26	7	a1i	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to 0 \in V$
27	8	a1i	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to 1 \in V$
28		ovexd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A B \in V$
29		ovexd	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A C \in V$
30		fveq2	$⊢ x = 0 \to (\{0, 1\} \times \{A\}) (x) = (\{0, 1\} \times \{A\}) (0)$
31		fveq2	$⊢ x = 0 \to \{⟨0, B⟩, ⟨1, C⟩\} (x) = \{⟨0, B⟩, ⟨1, C⟩\} (0)$
32	30 31	oveq12d	$⊢ x = 0 \to (\{0, 1\} \times \{A\}) (x) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (x) = (\{0, 1\} \times \{A\}) (0) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (0)$
33		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
34	33	eqcomi	$⊢ \cdot_{ℤ_{ring}} = \times$
35	34	a1i	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to \cdot_{ℤ_{ring}} = \times$
36	7	prid1	$⊢ 0 \in \{0, 1\}$
37		fvconst2g	$⊢ (A \in ℤ \land 0 \in \{0, 1\}) \to (\{0, 1\} \times \{A\}) (0) = A$
38	19 36 37	sylancl	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (\{0, 1\} \times \{A\}) (0) = A$
39		simp2	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to B \in ℤ$
40		fvpr1g	$⊢ (0 \in V \land B \in ℤ \land 0 \neq 1) \to \{⟨0, B⟩, ⟨1, C⟩\} (0) = B$
41	26 39 13 40	syl3anc	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to \{⟨0, B⟩, ⟨1, C⟩\} (0) = B$
42	35 38 41	oveq123d	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (\{0, 1\} \times \{A\}) (0) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (0) = A B$
43	32 42	sylan9eqr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land x = 0) \to (\{0, 1\} \times \{A\}) (x) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (x) = A B$
44		fveq2	$⊢ x = 1 \to (\{0, 1\} \times \{A\}) (x) = (\{0, 1\} \times \{A\}) (1)$
45		fveq2	$⊢ x = 1 \to \{⟨0, B⟩, ⟨1, C⟩\} (x) = \{⟨0, B⟩, ⟨1, C⟩\} (1)$
46	44 45	oveq12d	$⊢ x = 1 \to (\{0, 1\} \times \{A\}) (x) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (x) = (\{0, 1\} \times \{A\}) (1) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (1)$
47	8	prid2	$⊢ 1 \in \{0, 1\}$
48		fvconst2g	$⊢ (A \in ℤ \land 1 \in \{0, 1\}) \to (\{0, 1\} \times \{A\}) (1) = A$
49	19 47 48	sylancl	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (\{0, 1\} \times \{A\}) (1) = A$
50		simp3	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to C \in ℤ$
51		fvpr2g	$⊢ (1 \in V \land C \in ℤ \land 0 \neq 1) \to \{⟨0, B⟩, ⟨1, C⟩\} (1) = C$
52	27 50 13 51	syl3anc	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to \{⟨0, B⟩, ⟨1, C⟩\} (1) = C$
53	35 49 52	oveq123d	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to (\{0, 1\} \times \{A\}) (1) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (1) = A C$
54	46 53	sylan9eqr	$⊢ ((A \in ℤ \land B \in ℤ \land C \in ℤ) \land x = 1) \to (\{0, 1\} \times \{A\}) (x) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (x) = A C$
55	26 27 28 29 43 54	fmptpr	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to \{⟨0, A B⟩, ⟨1, A C⟩\} = (x \in \{0, 1\} ⟼ (\{0, 1\} \times \{A\}) (x) \cdot_{ℤ_{ring}} \{⟨0, B⟩, ⟨1, C⟩\} (x))$
56	16 25 55	3eqtr4d	$⊢ (A \in ℤ \land B \in ℤ \land C \in ℤ) \to A \underset{˙}{∙} \{⟨0, B⟩, ⟨1, C⟩\} = \{⟨0, A B⟩, ⟨1, A C⟩\}$

Metamath Proof Explorer

Theorem zlmodzxzscm

Proof