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 ⊢ 𝑍 = ( ℤ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 , ( 𝐴 · 𝐶 ) ⟩ } )