Metamath Proof Explorer


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|xz=2x+1
oddinmgm.r M=fld𝑠O
Assertion oddiadd +=+M

Proof

Step Hyp Ref Expression
1 oddinmgm.e O=z|xz=2x+1
2 oddinmgm.r M=fld𝑠O
3 zex V
4 1 3 rabex2 OV
5 2 cnfldsrngadd OV+=+M
6 4 5 ax-mp +=+M