Theorem 2zrngasgrp

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

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

Proof

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