Metamath Proof Explorer

Theorem 2zrngmmgm

Description: R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2 2zrngbas.r ⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3 2zrngmmgm.1 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
4 eqeq1 ⊢ ( 𝑧 = 𝑎 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑎 = ( 2 · 𝑥 ) ) )
5 4 rexbidv ⊢ ( 𝑧 = 𝑎 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) )
6 5 1 elrab2 ⊢ ( 𝑎 ∈ 𝐸 ↔ ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) )
7 eqeq1 ⊢ ( 𝑧 = 𝑏 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑏 = ( 2 · 𝑥 ) ) )
8 7 rexbidv ⊢ ( 𝑧 = 𝑏 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) )
9 8 1 elrab2 ⊢ ( 𝑏 ∈ 𝐸 ↔ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) )
10 zmulcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
11 10 ad2ant2r ⊢ ( ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
12 nfv ⊢ Ⅎ 𝑥 𝑎 ∈ ℤ
13 nfv ⊢ Ⅎ 𝑥 𝑏 ∈ ℤ
14 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 )
15 13 14 nfan ⊢ Ⅎ 𝑥 ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) )
16 nfv ⊢ Ⅎ 𝑥 ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 )
17 15 16 nfim ⊢ Ⅎ 𝑥 ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) )
18 12 17 nfim ⊢ Ⅎ 𝑥 ( 𝑎 ∈ ℤ → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
19 simpll ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) → 𝑥 ∈ ℤ )
20 simpl ⊢ ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → 𝑏 ∈ ℤ )
21 zmulcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑥 · 𝑏 ) ∈ ℤ )
22 19 20 21 syl2an ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑥 · 𝑏 ) ∈ ℤ )
23 oveq2 ⊢ ( 𝑦 = ( 𝑥 · 𝑏 ) → ( 2 · 𝑦 ) = ( 2 · ( 𝑥 · 𝑏 ) ) )
24 23 eqeq2d ⊢ ( 𝑦 = ( 𝑥 · 𝑏 ) → ( ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ↔ ( 𝑎 · 𝑏 ) = ( 2 · ( 𝑥 · 𝑏 ) ) ) )
25 24 adantl ⊢ ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) ∧ 𝑦 = ( 𝑥 · 𝑏 ) ) → ( ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ↔ ( 𝑎 · 𝑏 ) = ( 2 · ( 𝑥 · 𝑏 ) ) ) )
26 oveq1 ⊢ ( 𝑎 = ( 2 · 𝑥 ) → ( 𝑎 · 𝑏 ) = ( ( 2 · 𝑥 ) · 𝑏 ) )
27 26 ad3antlr ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑎 · 𝑏 ) = ( ( 2 · 𝑥 ) · 𝑏 ) )
28 2cnd ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → 2 ∈ ℂ )
29 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
30 29 ad3antrrr ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → 𝑥 ∈ ℂ )
31 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
32 31 adantr ⊢ ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → 𝑏 ∈ ℂ )
33 32 adantl ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → 𝑏 ∈ ℂ )
34 28 30 33 mulassd ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( ( 2 · 𝑥 ) · 𝑏 ) = ( 2 · ( 𝑥 · 𝑏 ) ) )
35 27 34 eqtrd ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑎 · 𝑏 ) = ( 2 · ( 𝑥 · 𝑏 ) ) )
36 22 25 35 rspcedvd ⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) )
37 36 exp41 ⊢ ( 𝑥 ∈ ℤ → ( 𝑎 = ( 2 · 𝑥 ) → ( 𝑎 ∈ ℤ → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) ) ) )
38 18 37 rexlimi ⊢ ( ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) → ( 𝑎 ∈ ℤ → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) ) )
39 38 impcom ⊢ ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
40 39 imp ⊢ ( ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) )
41 eqeq1 ⊢ ( 𝑧 = ( 𝑎 · 𝑏 ) → ( 𝑧 = ( 2 · 𝑥 ) ↔ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ) )
42 41 rexbidv ⊢ ( 𝑧 = ( 𝑎 · 𝑏 ) → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ) )
43 42 1 elrab2 ⊢ ( ( 𝑎 · 𝑏 ) ∈ 𝐸 ↔ ( ( 𝑎 · 𝑏 ) ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ) )
44 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
45 44 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ↔ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
46 45 cbvrexvw ⊢ ( ∃ 𝑥 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ↔ ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) )
47 46 anbi2i ⊢ ( ( ( 𝑎 · 𝑏 ) ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ) ↔ ( ( 𝑎 · 𝑏 ) ∈ ℤ ∧ ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
48 43 47 bitri ⊢ ( ( 𝑎 · 𝑏 ) ∈ 𝐸 ↔ ( ( 𝑎 · 𝑏 ) ∈ ℤ ∧ ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
49 11 40 48 sylanbrc ⊢ ( ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐸 )
50 6 9 49 syl2anb ⊢ ( ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) → ( 𝑎 · 𝑏 ) ∈ 𝐸 )
51 50 rgen2 ⊢ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ∈ 𝐸
52 1 0even ⊢ 0 ∈ 𝐸
53 1 2 2zrngbas ⊢ 𝐸 = ( Base ‘ 𝑅 )
54 3 53 mgpbas ⊢ 𝐸 = ( Base ‘ 𝑀 )
55 1 2 2zrngmul ⊢ · = ( .r ‘ 𝑅 )
56 3 55 mgpplusg ⊢ · = ( +g ‘ 𝑀 )
57 54 56 ismgmn0 ⊢ ( 0 ∈ 𝐸 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ∈ 𝐸 ) )
58 52 57 ax-mp ⊢ ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ∈ 𝐸 )
59 51 58 mpbir ⊢ 𝑀 ∈ Mgm