Metamath Proof Explorer

Theorem 2zrngmmgm

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

Ref Expression
Hypotheses 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
2zrngmmgm.1 ⊢ M = mulGrp R
Assertion 2zrngmmgm ⊢ M ∈ Mgm

Proof

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