Metamath Proof Explorer

Theorem nvmf

Description: Mapping for the vector subtraction operation. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvmf.1 ⊢ X = BaseSet ⁡ U
nvmf.3 ⊢ M = - v ⁡ U
Assertion nvmf ⊢ U ∈ NrmCVec → M : X × X ⟶ X

Proof

Step Hyp Ref Expression
1 nvmf.1 ⊢ X = BaseSet ⁡ U
2 nvmf.3 ⊢ M = - v ⁡ U
3 simpl ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ y ∈ X → U ∈ NrmCVec
4 simprl ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ y ∈ X → x ∈ X
5 neg1cn ⊢ − 1 ∈ ℂ
6 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
7 1 6 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ y ∈ X → -1 ⋅ 𝑠OLD ⁡ U y ∈ X
8 5 7 mp3an2 ⊢ U ∈ NrmCVec ∧ y ∈ X → -1 ⋅ 𝑠OLD ⁡ U y ∈ X
9 8 adantrl ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ y ∈ X → -1 ⋅ 𝑠OLD ⁡ U y ∈ X
10 eqid ⊢ + v ⁡ U = + v ⁡ U
11 1 10 nvgcl ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U y ∈ X → x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y ∈ X
12 3 4 9 11 syl3anc ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ y ∈ X → x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y ∈ X
13 12 ralrimivva ⊢ U ∈ NrmCVec → ∀ x ∈ X ∀ y ∈ X x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y ∈ X
14 eqid ⊢ x ∈ X , y ∈ X ⟼ x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y = x ∈ X , y ∈ X ⟼ x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y
15 14 fmpo ⊢ ∀ x ∈ X ∀ y ∈ X x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y ∈ X ↔ x ∈ X , y ∈ X ⟼ x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y : X × X ⟶ X
16 13 15 sylib ⊢ U ∈ NrmCVec → x ∈ X , y ∈ X ⟼ x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y : X × X ⟶ X
17 1 10 6 2 nvmfval ⊢ U ∈ NrmCVec → M = x ∈ X , y ∈ X ⟼ x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y
18 17 feq1d ⊢ U ∈ NrmCVec → M : X × X ⟶ X ↔ x ∈ X , y ∈ X ⟼ x + v ⁡ U -1 ⋅ 𝑠OLD ⁡ U y : X × X ⟶ X
19 16 18 mpbird ⊢ U ∈ NrmCVec → M : X × X ⟶ X