Theorem cnnvm

Description: The vector subtraction operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cnnvm.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
Assertion	cnnvm	$$⊢-={-}_v\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnnvm.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
2		mulm1	$$⊢y\in ℂ\to -1y=-y$$
3	2	adantl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to -1y=-y$$
4	3	oveq2d	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x+-1y=x+\left(-y\right)$$
5		negsub	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x+\left(-y\right)=x-y$$
6	4 5	eqtr2d	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x-y=x+-1y$$
7	6	mpoeq3ia	$$⊢\left(x\in ℂ,y\in ℂ⟼x-y\right)=\left(x\in ℂ,y\in ℂ⟼x+-1y\right)$$
8		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
9		ffn	$$⊢-:ℂ\times ℂ⟶ℂ\to -Fn\left(ℂ\times ℂ\right)$$
10	8 9	ax-mp	$$⊢-Fn\left(ℂ\times ℂ\right)$$
11		fnov	$$⊢-Fn\left(ℂ\times ℂ\right)\leftrightarrow -=\left(x\in ℂ,y\in ℂ⟼x-y\right)$$
12	10 11	mpbi	$$⊢-=\left(x\in ℂ,y\in ℂ⟼x-y\right)$$
13	1	cnnv	$$⊢U\in \mathrm{NrmCVec}$$
14	1	cnnvba	$$⊢ℂ=\mathrm{BaseSet}\left(U\right)$$
15	1	cnnvg	$$⊢+={+}_v\left(U\right)$$
16	1	cnnvs	$$⊢\times ={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
17		eqid	$$⊢{-}_v\left(U\right)={-}_v\left(U\right)$$
18	14 15 16 17	nvmfval	$$⊢U\in \mathrm{NrmCVec}\to {-}_v\left(U\right)=\left(x\in ℂ,y\in ℂ⟼x+-1y\right)$$
19	13 18	ax-mp	$$⊢{-}_v\left(U\right)=\left(x\in ℂ,y\in ℂ⟼x+-1y\right)$$
20	7 12 19	3eqtr4i	$$⊢-={-}_v\left(U\right)$$