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	|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
	oddinmgm.r	|- M = ( CCfld |`s O )
Assertion	oddiadd	|- + = ( +g ` M )

Proof

Step	Hyp	Ref	Expression
1		oddinmgm.e	|- O = { z e. ZZ | E. x e. ZZ z = ( ( 2 x. x ) + 1 ) }
2		oddinmgm.r	|- M = ( CCfld |`s O )
3		zex	|- ZZ e. _V
4	1 3	rabex2	|- O e. _V
5	2	cnfldsrngadd	|- ( O e. _V -> + = ( +g ` M ) )
6	4 5	ax-mp	|- + = ( +g ` M )