Metamath Proof Explorer

Theorem 2zrngasgrp

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

Ref Expression
Hypotheses 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
Assertion 2zrngasgrp Could not format assertion : No typesetting found for |- R e. Smgrp with typecode |-

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2 2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
3 1 2 2zrngamgm ⊢ R ∈ Mgm
4 elrabi ⊢ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → a ∈ ℤ
5 elrabi ⊢ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → y ∈ ℤ
6 elrabi ⊢ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → b ∈ ℤ
7 4 5 6 3anim123i ⊢ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∧ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x ∧ b ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → a ∈ ℤ ∧ y ∈ ℤ ∧ b ∈ ℤ
8 zcn ⊢ a ∈ ℤ → a ∈ ℂ
9 zcn ⊢ y ∈ ℤ → y ∈ ℂ
10 zcn ⊢ b ∈ ℤ → b ∈ ℂ
11 8 9 10 3anim123i ⊢ a ∈ ℤ ∧ y ∈ ℤ ∧ b ∈ ℤ → a ∈ ℂ ∧ y ∈ ℂ ∧ b ∈ ℂ
12 addass ⊢ a ∈ ℂ ∧ y ∈ ℂ ∧ b ∈ ℂ → a + y + b = a + y + b
13 7 11 12 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
14 13 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
15 1 2 2zrngbas ⊢ E = Base R
16 1 15 eqtr3i ⊢ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x = Base R
17 1 2 2zrngadd ⊢ + = + R
18 16 17 issgrp Could not format ( R e. Smgrp <-> ( R e. Mgm /\ A. a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ( ( a + y ) + b ) = ( a + ( y + b ) ) ) ) : No typesetting found for |- ( R e. Smgrp <-> ( R e. Mgm /\ A. a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ( ( a + y ) + b ) = ( a + ( y + b ) ) ) ) with typecode |-
19 3 14 18 mpbir2an Could not format R e. Smgrp : No typesetting found for |- R e. Smgrp with typecode |-