Metamath Proof Explorer


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 − = ( −𝑣𝑈 )