Theorem cnfldplusf

Description: The functionalized addition operation of the field of complex numbers. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Assertion	cnfldplusf	$$⊢+={+}_{𝑓}\left({ℂ}_{\mathrm{fld}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-addf	$$⊢+:ℂ\times ℂ⟶ℂ$$
2		ffn	$$⊢+:ℂ\times ℂ⟶ℂ\to +Fn\left(ℂ\times ℂ\right)$$
3		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
4		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
5		eqid	$$⊢{+}_{𝑓}\left({ℂ}_{\mathrm{fld}}\right)={+}_{𝑓}\left({ℂ}_{\mathrm{fld}}\right)$$
6	3 4 5	plusfeq	$$⊢+Fn\left(ℂ\times ℂ\right)\to {+}_{𝑓}\left({ℂ}_{\mathrm{fld}}\right)=+$$
7	1 2 6	mp2b	$$⊢{+}_{𝑓}\left({ℂ}_{\mathrm{fld}}\right)=+$$
8	7	eqcomi	$$⊢+={+}_{𝑓}\left({ℂ}_{\mathrm{fld}}\right)$$