# 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 $⊢ U = + × abs$
Assertion cnnvm $⊢ − = - v ⁡ U$

### Proof

Step Hyp Ref Expression
1 cnnvm.6 $⊢ U = + × abs$
2 mulm1 $⊢ y ∈ ℂ → -1 ⁢ y = − y$
3 2 adantl $⊢ x ∈ ℂ ∧ y ∈ ℂ → -1 ⁢ y = − y$
4 3 oveq2d $⊢ x ∈ ℂ ∧ y ∈ ℂ → x + -1 ⁢ y = x + − y$
5 negsub $⊢ x ∈ ℂ ∧ y ∈ ℂ → x + − y = x − y$
6 4 5 eqtr2d $⊢ x ∈ ℂ ∧ y ∈ ℂ → x − y = x + -1 ⁢ y$
7 6 mpoeq3ia $⊢ x ∈ ℂ , y ∈ ℂ ⟼ x − y = x ∈ ℂ , y ∈ ℂ ⟼ x + -1 ⁢ y$
8 subf $⊢ − : ℂ × ℂ ⟶ ℂ$
9 ffn $⊢ − : ℂ × ℂ ⟶ ℂ → − Fn ℂ × ℂ$
10 8 9 ax-mp $⊢ − Fn ℂ × ℂ$
11 fnov $⊢ − Fn ℂ × ℂ ↔ − = x ∈ ℂ , y ∈ ℂ ⟼ x − y$
12 10 11 mpbi $⊢ − = x ∈ ℂ , y ∈ ℂ ⟼ x − y$
13 1 cnnv $⊢ U ∈ NrmCVec$
14 1 cnnvba $⊢ ℂ = BaseSet ⁡ U$
15 1 cnnvg $⊢ + = + v ⁡ U$
16 1 cnnvs $⊢ × = ⋅ 𝑠OLD ⁡ U$
17 eqid $⊢ - v ⁡ U = - v ⁡ U$
18 14 15 16 17 nvmfval $⊢ U ∈ NrmCVec → - v ⁡ U = x ∈ ℂ , y ∈ ℂ ⟼ x + -1 ⁢ y$
19 13 18 ax-mp $⊢ - v ⁡ U = x ∈ ℂ , y ∈ ℂ ⟼ x + -1 ⁢ y$
20 7 12 19 3eqtr4i $⊢ − = - v ⁡ U$