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 = ( ZZring freeLMod { 0 , 1 } )
zlmodzxzscm.t 
|- .xb = ( .s ` Z )
Assertion zlmodzxzscm 
|- ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A .xb { <. 0 , B >. , <. 1 , C >. } ) = { <. 0 , ( A x. B ) >. , <. 1 , ( A x. C ) >. } )

Proof

Step Hyp Ref Expression
1 zlmodzxz.z 
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 zlmodzxzscm.t 
 |-  .xb = ( .s ` Z )
3 prex 
 |-  { 0 , 1 } e. _V
4 3 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> { 0 , 1 } e. _V )
5 fnconstg 
 |-  ( A e. ZZ -> ( { 0 , 1 } X. { A } ) Fn { 0 , 1 } )
6 5 3ad2ant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( { 0 , 1 } X. { A } ) Fn { 0 , 1 } )
7 c0ex 
 |-  0 e. _V
8 1ex 
 |-  1 e. _V
9 7 8 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
10 9 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( 0 e. _V /\ 1 e. _V ) )
11 3simpc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( B e. ZZ /\ C e. ZZ ) )
12 0ne1 
 |-  0 =/= 1
13 12 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> 0 =/= 1 )
14 fnprg 
 |-  ( ( ( 0 e. _V /\ 1 e. _V ) /\ ( B e. ZZ /\ C e. ZZ ) /\ 0 =/= 1 ) -> { <. 0 , B >. , <. 1 , C >. } Fn { 0 , 1 } )
15 10 11 13 14 syl3anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> { <. 0 , B >. , <. 1 , C >. } Fn { 0 , 1 } )
16 4 6 15 offvalfv 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( { 0 , 1 } X. { A } ) oF ( .r ` ZZring ) { <. 0 , B >. , <. 1 , C >. } ) = ( x e. { 0 , 1 } |-> ( ( ( { 0 , 1 } X. { A } ) ` x ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` x ) ) ) )
17 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
18 eqid 
 |-  ( Base ` ZZring ) = ( Base ` ZZring )
19 simp1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> A e. ZZ )
20 zringbas 
 |-  ZZ = ( Base ` ZZring )
21 19 20 eleqtrdi 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> A e. ( Base ` ZZring ) )
22 1 zlmodzxzel 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> { <. 0 , B >. , <. 1 , C >. } e. ( Base ` Z ) )
23 22 3adant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> { <. 0 , B >. , <. 1 , C >. } e. ( Base ` Z ) )
24 eqid 
 |-  ( .r ` ZZring ) = ( .r ` ZZring )
25 1 17 18 4 21 23 2 24 frlmvscafval 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A .xb { <. 0 , B >. , <. 1 , C >. } ) = ( ( { 0 , 1 } X. { A } ) oF ( .r ` ZZring ) { <. 0 , B >. , <. 1 , C >. } ) )
26 7 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> 0 e. _V )
27 8 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> 1 e. _V )
28 ovexd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A x. B ) e. _V )
29 ovexd 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A x. C ) e. _V )
30 fveq2 
 |-  ( x = 0 -> ( ( { 0 , 1 } X. { A } ) ` x ) = ( ( { 0 , 1 } X. { A } ) ` 0 ) )
31 fveq2 
 |-  ( x = 0 -> ( { <. 0 , B >. , <. 1 , C >. } ` x ) = ( { <. 0 , B >. , <. 1 , C >. } ` 0 ) )
32 30 31 oveq12d 
 |-  ( x = 0 -> ( ( ( { 0 , 1 } X. { A } ) ` x ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` x ) ) = ( ( ( { 0 , 1 } X. { A } ) ` 0 ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` 0 ) ) )
33 zringmulr 
 |-  x. = ( .r ` ZZring )
34 33 eqcomi 
 |-  ( .r ` ZZring ) = x.
35 34 a1i 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( .r ` ZZring ) = x. )
36 7 prid1 
 |-  0 e. { 0 , 1 }
37 fvconst2g 
 |-  ( ( A e. ZZ /\ 0 e. { 0 , 1 } ) -> ( ( { 0 , 1 } X. { A } ) ` 0 ) = A )
38 19 36 37 sylancl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( { 0 , 1 } X. { A } ) ` 0 ) = A )
39 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> B e. ZZ )
40 fvpr1g 
 |-  ( ( 0 e. _V /\ B e. ZZ /\ 0 =/= 1 ) -> ( { <. 0 , B >. , <. 1 , C >. } ` 0 ) = B )
41 26 39 13 40 syl3anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( { <. 0 , B >. , <. 1 , C >. } ` 0 ) = B )
42 35 38 41 oveq123d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( ( { 0 , 1 } X. { A } ) ` 0 ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` 0 ) ) = ( A x. B ) )
43 32 42 sylan9eqr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ x = 0 ) -> ( ( ( { 0 , 1 } X. { A } ) ` x ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` x ) ) = ( A x. B ) )
44 fveq2 
 |-  ( x = 1 -> ( ( { 0 , 1 } X. { A } ) ` x ) = ( ( { 0 , 1 } X. { A } ) ` 1 ) )
45 fveq2 
 |-  ( x = 1 -> ( { <. 0 , B >. , <. 1 , C >. } ` x ) = ( { <. 0 , B >. , <. 1 , C >. } ` 1 ) )
46 44 45 oveq12d 
 |-  ( x = 1 -> ( ( ( { 0 , 1 } X. { A } ) ` x ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` x ) ) = ( ( ( { 0 , 1 } X. { A } ) ` 1 ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` 1 ) ) )
47 8 prid2 
 |-  1 e. { 0 , 1 }
48 fvconst2g 
 |-  ( ( A e. ZZ /\ 1 e. { 0 , 1 } ) -> ( ( { 0 , 1 } X. { A } ) ` 1 ) = A )
49 19 47 48 sylancl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( { 0 , 1 } X. { A } ) ` 1 ) = A )
50 simp3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> C e. ZZ )
51 fvpr2g 
 |-  ( ( 1 e. _V /\ C e. ZZ /\ 0 =/= 1 ) -> ( { <. 0 , B >. , <. 1 , C >. } ` 1 ) = C )
52 27 50 13 51 syl3anc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( { <. 0 , B >. , <. 1 , C >. } ` 1 ) = C )
53 35 49 52 oveq123d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( ( { 0 , 1 } X. { A } ) ` 1 ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` 1 ) ) = ( A x. C ) )
54 46 53 sylan9eqr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ x = 1 ) -> ( ( ( { 0 , 1 } X. { A } ) ` x ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` x ) ) = ( A x. C ) )
55 26 27 28 29 43 54 fmptpr 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> { <. 0 , ( A x. B ) >. , <. 1 , ( A x. C ) >. } = ( x e. { 0 , 1 } |-> ( ( ( { 0 , 1 } X. { A } ) ` x ) ( .r ` ZZring ) ( { <. 0 , B >. , <. 1 , C >. } ` x ) ) ) )
56 16 25 55 3eqtr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A .xb { <. 0 , B >. , <. 1 , C >. } ) = { <. 0 , ( A x. B ) >. , <. 1 , ( A x. C ) >. } )