This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnrbas

Description: The set of complex numbers is the base set of the complex left module of complex numbers. (Contributed by AV, 21-Sep-2021)

Ref Expression
Hypothesis cnrlmod.c ⊢ C = ringLMod ⁡ ℂ fld
Assertion cnrbas ⊢ Base C = ℂ

Proof

Step Hyp Ref Expression
1 cnrlmod.c ⊢ C = ringLMod ⁡ ℂ fld
2 rlmbas ⊢ Base ℂ fld = Base ringLMod ⁡ ℂ fld
3 cnfldbas ⊢ ℂ = Base ℂ fld
4 1 fveq2i ⊢ Base C = Base ringLMod ⁡ ℂ fld
5 2 3 4 3eqtr4ri ⊢ Base C = ℂ