# Metamath Proof Explorer

## 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 ${⊢}{Z}={ℤ}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$
zlmodzxzscm.t
Assertion zlmodzxzscm

### Proof

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