Metamath Proof Explorer


Theorem cnfldsrngadd

Description: The group addition operation of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020)

Ref Expression
Hypothesis cnfldsrngbas.r R = fld 𝑠 S
Assertion cnfldsrngadd S V + = + R

Proof

Step Hyp Ref Expression
1 cnfldsrngbas.r R = fld 𝑠 S
2 cnfldadd + = + fld
3 1 2 ressplusg S V + = + R