Metamath Proof Explorer

Theorem cnfldsrngbas

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

Ref Expression
Hypothesis cnfldsrngbas.r 
|- R = ( CCfld |`s S )
Assertion cnfldsrngbas 
|- ( S C_ CC -> S = ( Base ` R ) )

Proof

Step Hyp Ref Expression
1 cnfldsrngbas.r 
 |-  R = ( CCfld |`s S )
2 cnfldbas 
 |-  CC = ( Base ` CCfld )
3 1 2 ressbas2 
 |-  ( S C_ CC -> S = ( Base ` R ) )