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 = ring freeLMod 0 1
zlmodzxzscm.t ˙ = Z
Assertion zlmodzxzscm A B C A ˙ 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 ˙ = Z
3 prex 0 1 V
4 3 a1i A B C 0 1 V
5 fnconstg A 0 1 × A Fn 0 1
6 5 3ad2ant1 A B C 0 1 × A Fn 0 1
7 c0ex 0 V
8 1ex 1 V
9 7 8 pm3.2i 0 V 1 V
10 9 a1i A B C 0 V 1 V
11 3simpc A B C B C
12 0ne1 0 1
13 12 a1i A B C 0 1
14 fnprg 0 V 1 V B C 0 1 0 B 1 C Fn 0 1
15 10 11 13 14 syl3anc A B C 0 B 1 C Fn 0 1
16 4 6 15 offvalfv A B C 0 1 × A ring f 0 B 1 C = x 0 1 0 1 × A x ring 0 B 1 C x
17 eqid Base Z = Base Z
18 eqid Base ring = Base ring
19 simp1 A B C A
20 zringbas = Base ring
21 19 20 syl6eleq A B C A Base ring
22 1 zlmodzxzel B C 0 B 1 C Base Z
23 22 3adant1 A B C 0 B 1 C Base Z
24 eqid ring = ring
25 1 17 18 4 21 23 2 24 frlmvscafval A B C A ˙ 0 B 1 C = 0 1 × A ring f 0 B 1 C
26 7 a1i A B C 0 V
27 8 a1i A B C 1 V
28 ovexd A B C A B V
29 ovexd A B C A C V
30 fveq2 x = 0 0 1 × A x = 0 1 × A 0
31 fveq2 x = 0 0 B 1 C x = 0 B 1 C 0
32 30 31 oveq12d x = 0 0 1 × A x ring 0 B 1 C x = 0 1 × A 0 ring 0 B 1 C 0
33 zringmulr × = ring
34 33 eqcomi ring = ×
35 34 a1i A B C ring = ×
36 7 prid1 0 0 1
37 fvconst2g A 0 0 1 0 1 × A 0 = A
38 19 36 37 sylancl A B C 0 1 × A 0 = A
39 simp2 A B C B
40 fvpr1g 0 V B 0 1 0 B 1 C 0 = B
41 26 39 13 40 syl3anc A B C 0 B 1 C 0 = B
42 35 38 41 oveq123d A B C 0 1 × A 0 ring 0 B 1 C 0 = A B
43 32 42 sylan9eqr A B C x = 0 0 1 × A x ring 0 B 1 C x = A B
44 fveq2 x = 1 0 1 × A x = 0 1 × A 1
45 fveq2 x = 1 0 B 1 C x = 0 B 1 C 1
46 44 45 oveq12d x = 1 0 1 × A x ring 0 B 1 C x = 0 1 × A 1 ring 0 B 1 C 1
47 8 prid2 1 0 1
48 fvconst2g A 1 0 1 0 1 × A 1 = A
49 19 47 48 sylancl A B C 0 1 × A 1 = A
50 simp3 A B C C
51 fvpr2g 1 V C 0 1 0 B 1 C 1 = C
52 27 50 13 51 syl3anc A B C 0 B 1 C 1 = C
53 35 49 52 oveq123d A B C 0 1 × A 1 ring 0 B 1 C 1 = A C
54 46 53 sylan9eqr A B C x = 1 0 1 × A x ring 0 B 1 C x = A C
55 26 27 28 29 43 54 fmptpr A B C 0 A B 1 A C = x 0 1 0 1 × A x ring 0 B 1 C x
56 16 25 55 3eqtr4d A B C A ˙ 0 B 1 C = 0 A B 1 A C