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 ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
zlmodzxzadd.p ⊢ + = ( +g ‘ 𝑍 )
Assertion zlmodzxzadd ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } + { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , ( 𝐴 + 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 + 𝐷 ) ⟩ } )

Proof

Step Hyp Ref Expression
1 zlmodzxz.z ⊢ 𝑍 = ( ℤring freeLMod { 0 , 1 } )
2 zlmodzxzadd.p ⊢ + = ( +g ‘ 𝑍 )
3 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
4 zringring ⊢ ℤring ∈ Ring
5 4 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ℤring ∈ Ring )
6 prex ⊢ { 0 , 1 } ∈ V
7 6 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { 0 , 1 } ∈ V )
8 simpl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
9 simpl ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → 𝐶 ∈ ℤ )
10 1 zlmodzxzel ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) )
11 8 9 10 syl2an ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∈ ( Base ‘ 𝑍 ) )
12 simpr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℤ )
13 simpr ⊢ ( ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → 𝐷 ∈ ℤ )
14 1 zlmodzxzel ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ∈ ( Base ‘ 𝑍 ) )
15 12 13 14 syl2an ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ∈ ( Base ‘ 𝑍 ) )
16 eqid ⊢ ( +g ‘ ℤring ) = ( +g ‘ ℤring )
17 1 3 5 7 11 15 16 2 frlmplusgval ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } + { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∘f ( +g ‘ ℤring ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) )
18 c0ex ⊢ 0 ∈ V
19 1ex ⊢ 1 ∈ V
20 18 19 pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V )
21 20 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 0 ∈ V ∧ 1 ∈ V ) )
22 8 9 anim12i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) )
23 0ne1 ⊢ 0 ≠ 1
24 23 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 0 ≠ 1 )
25 fnprg ⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ) ∧ ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ 0 ≠ 1 ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } Fn { 0 , 1 } )
26 21 22 24 25 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } Fn { 0 , 1 } )
27 12 13 anim12i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) )
28 fnprg ⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ 0 ≠ 1 ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } Fn { 0 , 1 } )
29 21 27 24 28 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } Fn { 0 , 1 } )
30 7 26 29 offvalfv ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ∘f ( +g ‘ ℤring ) { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = ( 𝑥 ∈ { 0 , 1 } ↦ ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 𝑥 ) ) ) )
31 18 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 0 ∈ V )
32 19 a1i ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 1 ∈ V )
33 ovexd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 𝐴 ( +g ‘ ℤring ) 𝐵 ) ∈ V )
34 ovexd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 𝐶 ( +g ‘ ℤring ) 𝐷 ) ∈ V )
35 fveq2 ⊢ ( 𝑥 = 0 → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) )
36 fveq2 ⊢ ( 𝑥 = 0 → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 𝑥 ) = ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 0 ) )
37 35 36 oveq12d ⊢ ( 𝑥 = 0 → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 𝑥 ) ) = ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 0 ) ) )
38 8 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 𝐴 ∈ ℤ )
39 fvpr1g ⊢ ( ( 0 ∈ V ∧ 𝐴 ∈ ℤ ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) = 𝐴 )
40 31 38 24 39 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) = 𝐴 )
41 12 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 𝐵 ∈ ℤ )
42 fvpr1g ⊢ ( ( 0 ∈ V ∧ 𝐵 ∈ ℤ ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 0 ) = 𝐵 )
43 31 41 24 42 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 0 ) = 𝐵 )
44 40 43 oveq12d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 0 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 0 ) ) = ( 𝐴 ( +g ‘ ℤring ) 𝐵 ) )
45 37 44 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝑥 = 0 ) → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 𝑥 ) ) = ( 𝐴 ( +g ‘ ℤring ) 𝐵 ) )
46 fveq2 ⊢ ( 𝑥 = 1 → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) = ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) )
47 fveq2 ⊢ ( 𝑥 = 1 → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 𝑥 ) = ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) )
48 46 47 oveq12d ⊢ ( 𝑥 = 1 → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 𝑥 ) ) = ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) )
49 9 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 𝐶 ∈ ℤ )
50 fvpr2g ⊢ ( ( 1 ∈ V ∧ 𝐶 ∈ ℤ ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) = 𝐶 )
51 32 49 24 50 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) = 𝐶 )
52 13 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → 𝐷 ∈ ℤ )
53 fvpr2g ⊢ ( ( 1 ∈ V ∧ 𝐷 ∈ ℤ ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) = 𝐷 )
54 32 52 24 53 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) = 𝐷 )
55 51 54 oveq12d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 1 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) = ( 𝐶 ( +g ‘ ℤring ) 𝐷 ) )
56 48 55 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) ∧ 𝑥 = 1 ) → ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 𝑥 ) ) = ( 𝐶 ( +g ‘ ℤring ) 𝐷 ) )
57 31 32 33 34 45 56 fmptpr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → { ⟨ 0 , ( 𝐴 ( +g ‘ ℤring ) 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 ( +g ‘ ℤring ) 𝐷 ) ⟩ } = ( 𝑥 ∈ { 0 , 1 } ↦ ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 𝑥 ) ) ) )
58 zringplusg ⊢ + = ( +g ‘ ℤring )
59 58 eqcomi ⊢ ( +g ‘ ℤring ) = +
60 59 oveqi ⊢ ( 𝐴 ( +g ‘ ℤring ) 𝐵 ) = ( 𝐴 + 𝐵 )
61 60 opeq2i ⊢ ⟨ 0 , ( 𝐴 ( +g ‘ ℤring ) 𝐵 ) ⟩ = ⟨ 0 , ( 𝐴 + 𝐵 ) ⟩
62 59 oveqi ⊢ ( 𝐶 ( +g ‘ ℤring ) 𝐷 ) = ( 𝐶 + 𝐷 )
63 62 opeq2i ⊢ ⟨ 1 , ( 𝐶 ( +g ‘ ℤring ) 𝐷 ) ⟩ = ⟨ 1 , ( 𝐶 + 𝐷 ) ⟩
64 61 63 preq12i ⊢ { ⟨ 0 , ( 𝐴 ( +g ‘ ℤring ) 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 ( +g ‘ ℤring ) 𝐷 ) ⟩ } = { ⟨ 0 , ( 𝐴 + 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 + 𝐷 ) ⟩ }
65 57 64 eqtr3di ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( 𝑥 ∈ { 0 , 1 } ↦ ( ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } ‘ 𝑥 ) ( +g ‘ ℤring ) ( { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ‘ 𝑥 ) ) ) = { ⟨ 0 , ( 𝐴 + 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 + 𝐷 ) ⟩ } )
66 17 30 65 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ) → ( { ⟨ 0 , 𝐴 ⟩ , ⟨ 1 , 𝐶 ⟩ } + { ⟨ 0 , 𝐵 ⟩ , ⟨ 1 , 𝐷 ⟩ } ) = { ⟨ 0 , ( 𝐴 + 𝐵 ) ⟩ , ⟨ 1 , ( 𝐶 + 𝐷 ) ⟩ } )