Theorem oddiadd

Description: Lemma 2 for oddinmgm : The group addition operation of M is the addition of complex numbers. (Contributed by AV, 3-Feb-2020)

	Ref	Expression
Hypotheses	oddinmgm.e	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) }
	oddinmgm.r	⊢ 𝑀 = ( ℂfld ↾s 𝑂 )
Assertion	oddiadd	⊢ + = ( +g ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( ( 2 · 𝑥 ) + 1 ) }
2		oddinmgm.r	⊢ 𝑀 = ( ℂfld ↾s 𝑂 )
3		zex	⊢ ℤ ∈ V
4	1 3	rabex2	⊢ 𝑂 ∈ V
5	2	cnfldsrngadd	⊢ ( 𝑂 ∈ V → + = ( +g ‘ 𝑀 ) )
6	4 5	ax-mp	⊢ + = ( +g ‘ 𝑀 )