Theorem cnfldplusf

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

	Ref	Expression
Assertion	cnfldplusf	⊢ + = ( +𝑓 ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		ax-addf	⊢ + : ( ℂ × ℂ ) ⟶ ℂ
2		ffn	⊢ ( + : ( ℂ × ℂ ) ⟶ ℂ → + Fn ( ℂ × ℂ ) )
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4		cnfldadd	⊢ + = ( +g ‘ ℂfld )
5		eqid	⊢ ( +𝑓 ‘ ℂfld ) = ( +𝑓 ‘ ℂfld )
6	3 4 5	plusfeq	⊢ ( + Fn ( ℂ × ℂ ) → ( +𝑓 ‘ ℂfld ) = + )
7	1 2 6	mp2b	⊢ ( +𝑓 ‘ ℂfld ) = +
8	7	eqcomi	⊢ + = ( +𝑓 ‘ ℂfld )