Metamath Proof Explorer
Description: The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020)
|
|
Ref |
Expression |
|
Hypothesis |
cnfldsrngbas.r |
⊢ 𝑅 = ( ℂfld ↾s 𝑆 ) |
|
Assertion |
cnfldsrngbas |
⊢ ( 𝑆 ⊆ ℂ → 𝑆 = ( Base ‘ 𝑅 ) ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
cnfldsrngbas.r |
⊢ 𝑅 = ( ℂfld ↾s 𝑆 ) |
2 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
3 |
1 2
|
ressbas2 |
⊢ ( 𝑆 ⊆ ℂ → 𝑆 = ( Base ‘ 𝑅 ) ) |