Theorem 2zrngmsgrp

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

	Ref	Expression
Hypotheses	2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
	2zrngmmgm.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion	2zrngmsgrp	⊢ 𝑀 ∈ Smgrp

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3		2zrngmmgm.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
4	1 2 3	2zrngmmgm	⊢ 𝑀 ∈ Mgm
5		elrabi	⊢ ( 𝑎 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑎 ∈ ℤ )
6		elrabi	⊢ ( 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑦 ∈ ℤ )
7		elrabi	⊢ ( 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑏 ∈ ℤ )
8	5 6 7	3anim123i	⊢ ( ( 𝑎 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ∧ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ∧ 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ) → ( 𝑎 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ) )
9		zcn	⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
10		zcn	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
11		zcn	⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
12	9 10 11	3anim123i	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑏 ∈ ℂ ) )
13		mulass	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( ( 𝑎 · 𝑦 ) · 𝑏 ) = ( 𝑎 · ( 𝑦 · 𝑏 ) ) )
14	8 12 13	3syl	⊢ ( ( 𝑎 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ∧ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ∧ 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ) → ( ( 𝑎 · 𝑦 ) · 𝑏 ) = ( 𝑎 · ( 𝑦 · 𝑏 ) ) )
15	14	rgen3	⊢ ∀ 𝑎 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ∀ 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ( ( 𝑎 · 𝑦 ) · 𝑏 ) = ( 𝑎 · ( 𝑦 · 𝑏 ) )
16	1 2	2zrngbas	⊢ 𝐸 = ( Base ‘ 𝑅 )
17	3 16	mgpbas	⊢ 𝐸 = ( Base ‘ 𝑀 )
18	1 17	eqtr3i	⊢ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } = ( Base ‘ 𝑀 )
19	1 2	2zrngmul	⊢ · = ( .r ‘ 𝑅 )
20	3 19	mgpplusg	⊢ · = ( +g ‘ 𝑀 )
21	18 20	issgrp	⊢ ( 𝑀 ∈ Smgrp ↔ ( 𝑀 ∈ Mgm ∧ ∀ 𝑎 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ∀ 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } ( ( 𝑎 · 𝑦 ) · 𝑏 ) = ( 𝑎 · ( 𝑦 · 𝑏 ) ) ) )
22	4 15 21	mpbir2an	⊢ 𝑀 ∈ Smgrp