Theorem cnfldplusf

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

	Ref	Expression
Assertion	cnfldplusf	|- + = ( +f ` CCfld )

Proof

Step	Hyp	Ref	Expression
1		ax-addf	|- + : ( CC X. CC ) --> CC
2		ffn	|- ( + : ( CC X. CC ) --> CC -> + Fn ( CC X. CC ) )
3		cnfldbas	|- CC = ( Base ` CCfld )
4		cnfldadd	|- + = ( +g ` CCfld )
5		eqid	|- ( +f ` CCfld ) = ( +f ` CCfld )
6	3 4 5	plusfeq	|- ( + Fn ( CC X. CC ) -> ( +f ` CCfld ) = + )
7	1 2 6	mp2b	|- ( +f ` CCfld ) = +
8	7	eqcomi	|- + = ( +f ` CCfld )