Metamath Proof Explorer

Theorem 2zrngmsgrp

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

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

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 1 2 3 2zrngmmgm ⊢ M ∈ Mgm
5 elrabi ⊢ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → a ∈ ℤ
6 elrabi ⊢ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → y ∈ ℤ
7 elrabi ⊢ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → b ∈ ℤ
8 5 6 7 3anim123i ⊢ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∧ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∧ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → a ∈ ℤ ∧ y ∈ ℤ ∧ b ∈ ℤ
9 zcn ⊢ a ∈ ℤ → a ∈ ℂ
10 zcn ⊢ y ∈ ℤ → y ∈ ℂ
11 zcn ⊢ b ∈ ℤ → b ∈ ℂ
12 9 10 11 3anim123i ⊢ a ∈ ℤ ∧ y ∈ ℤ ∧ b ∈ ℤ → a ∈ ℂ ∧ y ∈ ℂ ∧ b ∈ ℂ
13 mulass ⊢ a ∈ ℂ ∧ y ∈ ℂ ∧ b ∈ ℂ → a ⁢ y ⁢ b = a ⁢ y ⁢ b
14 8 12 13 3syl ⊢ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∧ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∧ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → a ⁢ y ⁢ b = a ⁢ y ⁢ b
15 14 rgen3 ⊢ ∀ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∀ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∀ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x a ⁢ y ⁢ b = a ⁢ y ⁢ b
16 1 2 2zrngbas ⊢ E = Base R
17 3 16 mgpbas ⊢ E = Base M
18 1 17 eqtr3i ⊢ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x = Base M
19 1 2 2zrngmul ⊢ × = ⋅ R
20 3 19 mgpplusg ⊢ × = + M
21 18 20 issgrp ⊢ M ∈ Smgrp ↔ M ∈ Mgm ∧ ∀ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∀ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∀ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x a ⁢ y ⁢ b = a ⁢ y ⁢ b
22 4 15 21 mpbir2an ⊢ M ∈ Smgrp