Metamath Proof Explorer

Theorem zlmodzxzadd

Description: The addition of the ZZ-module ZZ X. ZZ . (Contributed by AV, 22-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxz.z 
|- Z = ( ZZring freeLMod { 0 , 1 } )
zlmodzxzadd.p 
|- .+ = ( +g ` Z )
Assertion zlmodzxzadd 
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .+ { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( A + B ) >. , <. 1 , ( C + D ) >. } )

Proof

Step Hyp Ref Expression
1 zlmodzxz.z 
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 zlmodzxzadd.p 
 |-  .+ = ( +g ` Z )
3 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
4 zringring 
 |-  ZZring e. Ring
5 4 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ZZring e. Ring )
6 prex 
 |-  { 0 , 1 } e. _V
7 6 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { 0 , 1 } e. _V )
8 simpl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> A e. ZZ )
9 simpl 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> C e. ZZ )
10 1 zlmodzxzel 
 |-  ( ( A e. ZZ /\ C e. ZZ ) -> { <. 0 , A >. , <. 1 , C >. } e. ( Base ` Z ) )
11 8 9 10 syl2an 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , A >. , <. 1 , C >. } e. ( Base ` Z ) )
12 simpr 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. ZZ )
13 simpr 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> D e. ZZ )
14 1 zlmodzxzel 
 |-  ( ( B e. ZZ /\ D e. ZZ ) -> { <. 0 , B >. , <. 1 , D >. } e. ( Base ` Z ) )
15 12 13 14 syl2an 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , B >. , <. 1 , D >. } e. ( Base ` Z ) )
16 eqid 
 |-  ( +g ` ZZring ) = ( +g ` ZZring )
17 1 3 5 7 11 15 16 2 frlmplusgval 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .+ { <. 0 , B >. , <. 1 , D >. } ) = ( { <. 0 , A >. , <. 1 , C >. } oF ( +g ` ZZring ) { <. 0 , B >. , <. 1 , D >. } ) )
18 c0ex 
 |-  0 e. _V
19 1ex 
 |-  1 e. _V
20 18 19 pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V )
21 20 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( 0 e. _V /\ 1 e. _V ) )
22 8 9 anim12i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( A e. ZZ /\ C e. ZZ ) )
23 0ne1 
 |-  0 =/= 1
24 23 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> 0 =/= 1 )
25 fnprg 
 |-  ( ( ( 0 e. _V /\ 1 e. _V ) /\ ( A e. ZZ /\ C e. ZZ ) /\ 0 =/= 1 ) -> { <. 0 , A >. , <. 1 , C >. } Fn { 0 , 1 } )
26 21 22 24 25 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , A >. , <. 1 , C >. } Fn { 0 , 1 } )
27 12 13 anim12i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( B e. ZZ /\ D e. ZZ ) )
28 fnprg 
 |-  ( ( ( 0 e. _V /\ 1 e. _V ) /\ ( B e. ZZ /\ D e. ZZ ) /\ 0 =/= 1 ) -> { <. 0 , B >. , <. 1 , D >. } Fn { 0 , 1 } )
29 21 27 24 28 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , B >. , <. 1 , D >. } Fn { 0 , 1 } )
30 7 26 29 offvalfv 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } oF ( +g ` ZZring ) { <. 0 , B >. , <. 1 , D >. } ) = ( x e. { 0 , 1 } |-> ( ( { <. 0 , A >. , <. 1 , C >. } ` x ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` x ) ) ) )
31 18 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> 0 e. _V )
32 19 a1i 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> 1 e. _V )
33 ovexd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( A ( +g ` ZZring ) B ) e. _V )
34 ovexd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( C ( +g ` ZZring ) D ) e. _V )
35 fveq2 
 |-  ( x = 0 -> ( { <. 0 , A >. , <. 1 , C >. } ` x ) = ( { <. 0 , A >. , <. 1 , C >. } ` 0 ) )
36 fveq2 
 |-  ( x = 0 -> ( { <. 0 , B >. , <. 1 , D >. } ` x ) = ( { <. 0 , B >. , <. 1 , D >. } ` 0 ) )
37 35 36 oveq12d 
 |-  ( x = 0 -> ( ( { <. 0 , A >. , <. 1 , C >. } ` x ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` x ) ) = ( ( { <. 0 , A >. , <. 1 , C >. } ` 0 ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` 0 ) ) )
38 8 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> A e. ZZ )
39 fvpr1g 
 |-  ( ( 0 e. _V /\ A e. ZZ /\ 0 =/= 1 ) -> ( { <. 0 , A >. , <. 1 , C >. } ` 0 ) = A )
40 31 38 24 39 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } ` 0 ) = A )
41 12 adantr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> B e. ZZ )
42 fvpr1g 
 |-  ( ( 0 e. _V /\ B e. ZZ /\ 0 =/= 1 ) -> ( { <. 0 , B >. , <. 1 , D >. } ` 0 ) = B )
43 31 41 24 42 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , B >. , <. 1 , D >. } ` 0 ) = B )
44 40 43 oveq12d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( { <. 0 , A >. , <. 1 , C >. } ` 0 ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` 0 ) ) = ( A ( +g ` ZZring ) B ) )
45 37 44 sylan9eqr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ x = 0 ) -> ( ( { <. 0 , A >. , <. 1 , C >. } ` x ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` x ) ) = ( A ( +g ` ZZring ) B ) )
46 fveq2 
 |-  ( x = 1 -> ( { <. 0 , A >. , <. 1 , C >. } ` x ) = ( { <. 0 , A >. , <. 1 , C >. } ` 1 ) )
47 fveq2 
 |-  ( x = 1 -> ( { <. 0 , B >. , <. 1 , D >. } ` x ) = ( { <. 0 , B >. , <. 1 , D >. } ` 1 ) )
48 46 47 oveq12d 
 |-  ( x = 1 -> ( ( { <. 0 , A >. , <. 1 , C >. } ` x ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` x ) ) = ( ( { <. 0 , A >. , <. 1 , C >. } ` 1 ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` 1 ) ) )
49 9 adantl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> C e. ZZ )
50 fvpr2g 
 |-  ( ( 1 e. _V /\ C e. ZZ /\ 0 =/= 1 ) -> ( { <. 0 , A >. , <. 1 , C >. } ` 1 ) = C )
51 32 49 24 50 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } ` 1 ) = C )
52 13 adantl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> D e. ZZ )
53 fvpr2g 
 |-  ( ( 1 e. _V /\ D e. ZZ /\ 0 =/= 1 ) -> ( { <. 0 , B >. , <. 1 , D >. } ` 1 ) = D )
54 32 52 24 53 syl3anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , B >. , <. 1 , D >. } ` 1 ) = D )
55 51 54 oveq12d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( { <. 0 , A >. , <. 1 , C >. } ` 1 ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` 1 ) ) = ( C ( +g ` ZZring ) D ) )
56 48 55 sylan9eqr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ x = 1 ) -> ( ( { <. 0 , A >. , <. 1 , C >. } ` x ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` x ) ) = ( C ( +g ` ZZring ) D ) )
57 31 32 33 34 45 56 fmptpr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> { <. 0 , ( A ( +g ` ZZring ) B ) >. , <. 1 , ( C ( +g ` ZZring ) D ) >. } = ( x e. { 0 , 1 } |-> ( ( { <. 0 , A >. , <. 1 , C >. } ` x ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` x ) ) ) )
58 zringplusg 
 |-  + = ( +g ` ZZring )
59 58 eqcomi 
 |-  ( +g ` ZZring ) = +
60 59 oveqi 
 |-  ( A ( +g ` ZZring ) B ) = ( A + B )
61 60 opeq2i 
 |-  <. 0 , ( A ( +g ` ZZring ) B ) >. = <. 0 , ( A + B ) >.
62 59 oveqi 
 |-  ( C ( +g ` ZZring ) D ) = ( C + D )
63 62 opeq2i 
 |-  <. 1 , ( C ( +g ` ZZring ) D ) >. = <. 1 , ( C + D ) >.
64 61 63 preq12i 
 |-  { <. 0 , ( A ( +g ` ZZring ) B ) >. , <. 1 , ( C ( +g ` ZZring ) D ) >. } = { <. 0 , ( A + B ) >. , <. 1 , ( C + D ) >. }
65 57 64 eqtr3di 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( x e. { 0 , 1 } |-> ( ( { <. 0 , A >. , <. 1 , C >. } ` x ) ( +g ` ZZring ) ( { <. 0 , B >. , <. 1 , D >. } ` x ) ) ) = { <. 0 , ( A + B ) >. , <. 1 , ( C + D ) >. } )
66 17 30 65 3eqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( { <. 0 , A >. , <. 1 , C >. } .+ { <. 0 , B >. , <. 1 , D >. } ) = { <. 0 , ( A + B ) >. , <. 1 , ( C + D ) >. } )