Theorem 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	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
	zlmodzxzscm.t	⊢ ∙ = ( ·𝑠 ‘ 𝑍 )
Assertion	zlmodzxzscm	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∙ { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ) = { ⟨ 0 , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1 , ( 𝐴 · 𝐶 ) ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2		zlmodzxzscm.t	⊢ ∙ = ( ·𝑠 ‘ 𝑍 )
3		prex	⊢ { 0 , 1 } ∈ V
4	3	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → { 0 , 1 } ∈ V )
5		fnconstg	⊢ ( 𝐴 ∈ ℤ → ( { 0 , 1 } × { 𝐴 } ) Fn { 0 , 1 } )
6	5	3ad2ant1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( { 0 , 1 } × { 𝐴 } ) Fn { 0 , 1 } )
7		c0ex	⊢ 0 ∈ V
8		1ex	⊢ 1 ∈ V
9	7 8	pm3.2i	⊢ ( 0 ∈ V ∧ 1 ∈ V )
10	9	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 0 ∈ V ∧ 1 ∈ V ) )
11		3simpc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) )
12		0ne1	⊢ 0 ≠ 1
13	12	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 0 ≠ 1 )
14		fnprg	⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 0 ≠ 1 ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } Fn { 0 , 1 } )
15	10 11 13 14	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } Fn { 0 , 1 } )
16	4 6 15	offvalfv	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( { 0 , 1 } × { 𝐴 } ) ∘f ( .r ‘ ℤring ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ) = ( 𝑥 ∈ { 0 , 1 } ↦ ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 𝑥 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ) ) )
17		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
18		eqid	⊢ ( Base ‘ ℤring ) = ( Base ‘ ℤring )
19		simp1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ℤ )
20		zringbas	⊢ ℤ = ( Base ‘ ℤring )
21	19 20	eleqtrdi	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∈ ( Base ‘ ℤring ) )
22	1	zlmodzxzel	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) )
23	22	3adant1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) )
24		eqid	⊢ ( .r ‘ ℤring ) = ( .r ‘ ℤring )
25	1 17 18 4 21 23 2 24	frlmvscafval	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∙ { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ) = ( ( { 0 , 1 } × { 𝐴 } ) ∘f ( .r ‘ ℤring ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ) )
26	7	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 0 ∈ V )
27	8	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 1 ∈ V )
28		ovexd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 · 𝐵 ) ∈ V )
29		ovexd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 · 𝐶 ) ∈ V )
30		fveq2	⊢ ( 𝑥 = 0 → ( ( { 0 , 1 } × { 𝐴 } ) ‘ 𝑥 ) = ( ( { 0 , 1 } × { 𝐴 } ) ‘ 0 ) )
31		fveq2	⊢ ( 𝑥 = 0 → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) = ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) )
32	30 31	oveq12d	⊢ ( 𝑥 = 0 → ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 𝑥 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ) = ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 0 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) ) )
33		zringmulr	⊢ · = ( .r ‘ ℤring )
34	33	eqcomi	⊢ ( .r ‘ ℤring ) = ·
35	34	a1i	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( .r ‘ ℤring ) = · )
36	7	prid1	⊢ 0 ∈ { 0 , 1 }
37		fvconst2g	⊢ ( ( 𝐴 ∈ ℤ ∧ 0 ∈ { 0 , 1 } ) → ( ( { 0 , 1 } × { 𝐴 } ) ‘ 0 ) = 𝐴 )
38	19 36 37	sylancl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( { 0 , 1 } × { 𝐴 } ) ‘ 0 ) = 𝐴 )
39		simp2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐵 ∈ ℤ )
40		fvpr1g	⊢ ( ( 0 ∈ V ∧ 𝐵 ∈ ℤ ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) = 𝐵 )
41	26 39 13 40	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) = 𝐵 )
42	35 38 41	oveq123d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 0 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) ) = ( 𝐴 · 𝐵 ) )
43	32 42	sylan9eqr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝑥 = 0 ) → ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 𝑥 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ) = ( 𝐴 · 𝐵 ) )
44		fveq2	⊢ ( 𝑥 = 1 → ( ( { 0 , 1 } × { 𝐴 } ) ‘ 𝑥 ) = ( ( { 0 , 1 } × { 𝐴 } ) ‘ 1 ) )
45		fveq2	⊢ ( 𝑥 = 1 → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) = ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) )
46	44 45	oveq12d	⊢ ( 𝑥 = 1 → ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 𝑥 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ) = ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 1 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) ) )
47	8	prid2	⊢ 1 ∈ { 0 , 1 }
48		fvconst2g	⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ∈ { 0 , 1 } ) → ( ( { 0 , 1 } × { 𝐴 } ) ‘ 1 ) = 𝐴 )
49	19 47 48	sylancl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( { 0 , 1 } × { 𝐴 } ) ‘ 1 ) = 𝐴 )
50		simp3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐶 ∈ ℤ )
51		fvpr2g	⊢ ( ( 1 ∈ V ∧ 𝐶 ∈ ℤ ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) = 𝐶 )
52	27 50 13 51	syl3anc	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) = 𝐶 )
53	35 49 52	oveq123d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 1 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) ) = ( 𝐴 · 𝐶 ) )
54	46 53	sylan9eqr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 𝑥 = 1 ) → ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 𝑥 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ) = ( 𝐴 · 𝐶 ) )
55	26 27 28 29 43 54	fmptpr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → { ⟨ 0 , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1 , ( 𝐴 · 𝐶 ) ⟩ } = ( 𝑥 ∈ { 0 , 1 } ↦ ( ( ( { 0 , 1 } × { 𝐴 } ) ‘ 𝑥 ) ( .r ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ) ) )
56	16 25 55	3eqtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( 𝐴 ∙ { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐶 ⟩ } ) = { ⟨ 0 , ( 𝐴 · 𝐵 ) ⟩ , ⟨ 1 , ( 𝐴 · 𝐶 ) ⟩ } )