Metamath Proof Explorer

Theorem 2zrngamgm

Description: R is an (additive) magma. (Contributed by AV, 6-Jan-2020)

Ref Expression
Hypotheses 2zrng.e ⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2zrngbas.r ⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
Assertion 2zrngamgm 𝑅 ∈ Mgm

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2 2zrngbas.r ⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3 eqeq1 ⊢ ( 𝑧 = 𝑎 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑎 = ( 2 · 𝑥 ) ) )
4 3 rexbidv ⊢ ( 𝑧 = 𝑎 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) )
5 4 1 elrab2 ⊢ ( 𝑎 ∈ 𝐸 ↔ ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) )
6 eqeq1 ⊢ ( 𝑧 = 𝑏 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑏 = ( 2 · 𝑥 ) ) )
7 6 rexbidv ⊢ ( 𝑧 = 𝑏 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) )
8 7 1 elrab2 ⊢ ( 𝑏 ∈ 𝐸 ↔ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) )
9 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
10 9 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑎 = ( 2 · 𝑥 ) ↔ 𝑎 = ( 2 · 𝑦 ) ) )
11 10 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ↔ ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) )
12 zaddcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
13 12 ancoms ⊢ ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
14 13 adantr ⊢ ( ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ∧ ( ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ∧ ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) ) ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
15 simpl ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) → 𝑦 ∈ ℤ )
16 simpl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) → 𝑥 ∈ ℤ )
17 zaddcl ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑦 + 𝑥 ) ∈ ℤ )
18 15 16 17 syl2anr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) → ( 𝑦 + 𝑥 ) ∈ ℤ )
19 18 adantr ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) → ( 𝑦 + 𝑥 ) ∈ ℤ )
20 oveq2 ⊢ ( 𝑧 = ( 𝑦 + 𝑥 ) → ( 2 · 𝑧 ) = ( 2 · ( 𝑦 + 𝑥 ) ) )
21 20 eqeq2d ⊢ ( 𝑧 = ( 𝑦 + 𝑥 ) → ( ( 2 · ( 𝑦 + 𝑥 ) ) = ( 2 · 𝑧 ) ↔ ( 2 · ( 𝑦 + 𝑥 ) ) = ( 2 · ( 𝑦 + 𝑥 ) ) ) )
22 21 adantl ⊢ ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) ∧ 𝑧 = ( 𝑦 + 𝑥 ) ) → ( ( 2 · ( 𝑦 + 𝑥 ) ) = ( 2 · 𝑧 ) ↔ ( 2 · ( 𝑦 + 𝑥 ) ) = ( 2 · ( 𝑦 + 𝑥 ) ) ) )
23 eqidd ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) → ( 2 · ( 𝑦 + 𝑥 ) ) = ( 2 · ( 𝑦 + 𝑥 ) ) )
24 19 22 23 rspcedvd ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) → ∃ 𝑧 ∈ ℤ ( 2 · ( 𝑦 + 𝑥 ) ) = ( 2 · 𝑧 ) )
25 simpr ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) → 𝑎 = ( 2 · 𝑦 ) )
26 simpr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) → 𝑏 = ( 2 · 𝑥 ) )
27 25 26 oveqan12rd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) → ( 𝑎 + 𝑏 ) = ( ( 2 · 𝑦 ) + ( 2 · 𝑥 ) ) )
28 27 adantr ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) → ( 𝑎 + 𝑏 ) = ( ( 2 · 𝑦 ) + ( 2 · 𝑥 ) ) )
29 2cnd ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) → 2 ∈ ℂ )
30 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
31 30 adantr ⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) → 𝑦 ∈ ℂ )
32 31 adantl ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) → 𝑦 ∈ ℂ )
33 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
34 33 adantr ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) → 𝑥 ∈ ℂ )
35 34 adantr ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) → 𝑥 ∈ ℂ )
36 29 32 35 adddid ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) → ( 2 · ( 𝑦 + 𝑥 ) ) = ( ( 2 · 𝑦 ) + ( 2 · 𝑥 ) ) )
37 36 adantr ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) → ( 2 · ( 𝑦 + 𝑥 ) ) = ( ( 2 · 𝑦 ) + ( 2 · 𝑥 ) ) )
38 28 37 eqtr4d ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) → ( 𝑎 + 𝑏 ) = ( 2 · ( 𝑦 + 𝑥 ) ) )
39 38 eqeq1d ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) → ( ( 𝑎 + 𝑏 ) = ( 2 · 𝑧 ) ↔ ( 2 · ( 𝑦 + 𝑥 ) ) = ( 2 · 𝑧 ) ) )
40 39 rexbidv ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) → ( ∃ 𝑧 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑧 ) ↔ ∃ 𝑧 ∈ ℤ ( 2 · ( 𝑦 + 𝑥 ) ) = ( 2 · 𝑧 ) ) )
41 24 40 mpbird ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) ∧ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ) → ∃ 𝑧 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑧 ) )
42 41 ex ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) ∧ ( 𝑦 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑦 ) ) ) → ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ∃ 𝑧 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑧 ) ) )
43 42 rexlimdvaa ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑏 = ( 2 · 𝑥 ) ) → ( ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) → ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ∃ 𝑧 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑧 ) ) ) )
44 43 rexlimiva ⊢ ( ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) → ( ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) → ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ∃ 𝑧 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑧 ) ) ) )
45 44 imp ⊢ ( ( ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ∧ ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) ) → ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ∃ 𝑧 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑧 ) ) )
46 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 2 · 𝑥 ) = ( 2 · 𝑧 ) )
47 46 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑎 + 𝑏 ) = ( 2 · 𝑥 ) ↔ ( 𝑎 + 𝑏 ) = ( 2 · 𝑧 ) ) )
48 47 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑥 ) ↔ ∃ 𝑧 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑧 ) )
49 45 48 syl6ibr ⊢ ( ( ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ∧ ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) ) → ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ∃ 𝑥 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑥 ) ) )
50 49 impcom ⊢ ( ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ∧ ( ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ∧ ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) ) ) → ∃ 𝑥 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑥 ) )
51 eqeq1 ⊢ ( 𝑧 = ( 𝑎 + 𝑏 ) → ( 𝑧 = ( 2 · 𝑥 ) ↔ ( 𝑎 + 𝑏 ) = ( 2 · 𝑥 ) ) )
52 51 rexbidv ⊢ ( 𝑧 = ( 𝑎 + 𝑏 ) → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑥 ) ) )
53 52 1 elrab2 ⊢ ( ( 𝑎 + 𝑏 ) ∈ 𝐸 ↔ ( ( 𝑎 + 𝑏 ) ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ ( 𝑎 + 𝑏 ) = ( 2 · 𝑥 ) ) )
54 14 50 53 sylanbrc ⊢ ( ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ∧ ( ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ∧ ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐸 )
55 54 exp32 ⊢ ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) → ( ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) → ( ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) → ( 𝑎 + 𝑏 ) ∈ 𝐸 ) ) )
56 55 impancom ⊢ ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ( 𝑎 ∈ ℤ → ( ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) → ( 𝑎 + 𝑏 ) ∈ 𝐸 ) ) )
57 56 com13 ⊢ ( ∃ 𝑦 ∈ ℤ 𝑎 = ( 2 · 𝑦 ) → ( 𝑎 ∈ ℤ → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐸 ) ) )
58 11 57 sylbi ⊢ ( ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) → ( 𝑎 ∈ ℤ → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐸 ) ) )
59 58 impcom ⊢ ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐸 ) )
60 59 imp ⊢ ( ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑎 + 𝑏 ) ∈ 𝐸 )
61 5 8 60 syl2anb ⊢ ( ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) → ( 𝑎 + 𝑏 ) ∈ 𝐸 )
62 61 rgen2 ⊢ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 + 𝑏 ) ∈ 𝐸
63 0z ⊢ 0 ∈ ℤ
64 2cn ⊢ 2 ∈ ℂ
65 0zd ⊢ ( 2 ∈ ℂ → 0 ∈ ℤ )
66 oveq2 ⊢ ( 𝑥 = 0 → ( 2 · 𝑥 ) = ( 2 · 0 ) )
67 66 eqeq2d ⊢ ( 𝑥 = 0 → ( 0 = ( 2 · 𝑥 ) ↔ 0 = ( 2 · 0 ) ) )
68 67 adantl ⊢ ( ( 2 ∈ ℂ ∧ 𝑥 = 0 ) → ( 0 = ( 2 · 𝑥 ) ↔ 0 = ( 2 · 0 ) ) )
69 mul01 ⊢ ( 2 ∈ ℂ → ( 2 · 0 ) = 0 )
70 69 eqcomd ⊢ ( 2 ∈ ℂ → 0 = ( 2 · 0 ) )
71 65 68 70 rspcedvd ⊢ ( 2 ∈ ℂ → ∃ 𝑥 ∈ ℤ 0 = ( 2 · 𝑥 ) )
72 64 71 ax-mp ⊢ ∃ 𝑥 ∈ ℤ 0 = ( 2 · 𝑥 )
73 eqeq1 ⊢ ( 𝑧 = 0 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 0 = ( 2 · 𝑥 ) ) )
74 73 rexbidv ⊢ ( 𝑧 = 0 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 0 = ( 2 · 𝑥 ) ) )
75 74 elrab ⊢ ( 0 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ↔ ( 0 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 0 = ( 2 · 𝑥 ) ) )
76 63 72 75 mpbir2an ⊢ 0 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
77 76 1 eleqtrri ⊢ 0 ∈ 𝐸
78 1 2 2zrngbas ⊢ 𝐸 = ( Base ‘ 𝑅 )
79 1 2 2zrngadd ⊢ + = ( +g ‘ 𝑅 )
80 78 79 ismgmn0 ⊢ ( 0 ∈ 𝐸 → ( 𝑅 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 + 𝑏 ) ∈ 𝐸 ) )
81 77 80 ax-mp ⊢ ( 𝑅 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 + 𝑏 ) ∈ 𝐸 )
82 62 81 mpbir ⊢ 𝑅 ∈ Mgm