Metamath Proof Explorer

Theorem 2zrngasgrp

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

		Ref	Expression
	Hypotheses	2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ 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 \in ℤ \| \exists x \in ℤ z = 2 x\}$
2		2zrngbas.r	$⊢ R = ℂ_{fld} ↾_{𝑠} E$
3	1 2	2zrngamgm	$⊢ R \in Mgm$
4		elrabi	$⊢ a \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \to a \in ℤ$
5		elrabi	$⊢ y \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \to y \in ℤ$
6		elrabi	$⊢ b \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \to b \in ℤ$
7	4 5 6	3anim123i	$⊢ (a \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \land y \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \land b \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\}) \to (a \in ℤ \land y \in ℤ \land b \in ℤ)$
8		zcn	$⊢ a \in ℤ \to a \in ℂ$
9		zcn	$⊢ y \in ℤ \to y \in ℂ$
10		zcn	$⊢ b \in ℤ \to b \in ℂ$
11	8 9 10	3anim123i	$⊢ (a \in ℤ \land y \in ℤ \land b \in ℤ) \to (a \in ℂ \land y \in ℂ \land b \in ℂ)$
12		addass	$⊢ (a \in ℂ \land y \in ℂ \land b \in ℂ) \to a + y + b = a + y + b$
13	7 11 12	3syl	$⊢ (a \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \land y \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \land b \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\}) \to a + y + b = a + y + b$
14	13	rgen3	$⊢ \forall a \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \forall y \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \forall b \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} a + y + b = a + y + b$
15	1 2	2zrngbas	$⊢ E = {Base}_{R}$
16	1 15	eqtr3i	$⊢ \{z \in ℤ \| \exists x \in ℤ 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 \|-