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	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
Assertion	cnnvm	⊢ − = ( −𝑣 ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		cnnvm.6	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
2		mulm1	⊢ ( 𝑦 ∈ ℂ → ( - 1 · 𝑦 ) = - 𝑦 )
3	2	adantl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( - 1 · 𝑦 ) = - 𝑦 )
4	3	oveq2d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + ( - 1 · 𝑦 ) ) = ( 𝑥 + - 𝑦 ) )
5		negsub	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + - 𝑦 ) = ( 𝑥 − 𝑦 ) )
6	4 5	eqtr2d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 − 𝑦 ) = ( 𝑥 + ( - 1 · 𝑦 ) ) )
7	6	mpoeq3ia	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 − 𝑦 ) ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + ( - 1 · 𝑦 ) ) )
8		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
9		ffn	⊢ ( − : ( ℂ × ℂ ) ⟶ ℂ → − Fn ( ℂ × ℂ ) )
10	8 9	ax-mp	⊢ − Fn ( ℂ × ℂ )
11		fnov	⊢ ( − Fn ( ℂ × ℂ ) ↔ − = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 − 𝑦 ) ) )
12	10 11	mpbi	⊢ − = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 − 𝑦 ) )
13	1	cnnv	⊢ 𝑈 ∈ NrmCVec
14	1	cnnvba	⊢ ℂ = ( BaseSet ‘ 𝑈 )
15	1	cnnvg	⊢ + = ( +𝑣 ‘ 𝑈 )
16	1	cnnvs	⊢ · = ( ·𝑠OLD ‘ 𝑈 )
17		eqid	⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
18	14 15 16 17	nvmfval	⊢ ( 𝑈 ∈ NrmCVec → ( −𝑣 ‘ 𝑈 ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + ( - 1 · 𝑦 ) ) ) )
19	13 18	ax-mp	⊢ ( −𝑣 ‘ 𝑈 ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + ( - 1 · 𝑦 ) ) )
20	7 12 19	3eqtr4i	⊢ − = ( −𝑣 ‘ 𝑈 )