Theorem 2zrngmsgrp

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

	Ref	Expression
Hypotheses	2zrng.e	$$⊢E=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}$$
	2zrngbas.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}E$$
	2zrngmmgm.1	$$⊢M={\mathrm{mulGrp}}_R$$
Assertion	2zrngmsgrp	Could not format assertion : No typesetting found for |- M e. Smgrp with typecode |-

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	$$⊢E=\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}$$
2		2zrngbas.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}E$$
3		2zrngmmgm.1	$$⊢M={\mathrm{mulGrp}}_R$$
4	1 2 3	2zrngmmgm	$$⊢M\in \mathrm{Mgm}$$
5		elrabi	$$⊢a\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\to a\in \mathbb{Z}$$
6		elrabi	$$⊢y\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\to y\in \mathbb{Z}$$
7		elrabi	$$⊢b\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\to b\in \mathbb{Z}$$
8	5 6 7	3anim123i	$$⊢\left(a\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\wedge y\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\wedge b\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\right)\to \left(a\in \mathbb{Z}\wedge y\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)$$
9		zcn	$$⊢a\in \mathbb{Z}\to a\in ℂ$$
10		zcn	$$⊢y\in \mathbb{Z}\to y\in ℂ$$
11		zcn	$$⊢b\in \mathbb{Z}\to b\in ℂ$$
12	9 10 11	3anim123i	$$⊢\left(a\in \mathbb{Z}\wedge y\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to \left(a\in ℂ\wedge y\in ℂ\wedge b\in ℂ\right)$$
13		mulass	$$⊢\left(a\in ℂ\wedge y\in ℂ\wedge b\in ℂ\right)\to ayb=ayb$$
14	8 12 13	3syl	$$⊢\left(a\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\wedge y\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\wedge b\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\right)\to ayb=ayb$$
15	14	rgen3	$$⊢\forall a\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\forall y\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}\forall b\in \left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}ayb=ayb$$
16	1 2	2zrngbas	$$⊢E={\mathrm{Base}}_R$$
17	3 16	mgpbas	$$⊢E={\mathrm{Base}}_M$$
18	1 17	eqtr3i	$$⊢\left\{z\in \mathbb{Z}|\exists x\in \mathbb{Z}z=2x\right\}={\mathrm{Base}}_M$$
19	1 2	2zrngmul	$$⊢\times ={\cdot }_R$$
20	3 19	mgpplusg	$$⊢\times ={+}_M$$
21	18 20	issgrp	Could not format ( M e. Smgrp <-> ( M 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 x. y ) x. b ) = ( a x. ( y x. b ) ) ) ) : No typesetting found for |- ( M e. Smgrp <-> ( M 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 x. y ) x. b ) = ( a x. ( y x. b ) ) ) ) with typecode |-
22	4 15 21	mpbir2an	Could not format M e. Smgrp : No typesetting found for |- M e. Smgrp with typecode |-