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⁡Uy∈X
8 5 7 mp3an2 ⊢U∈NrmCVec∧y∈X→-1⋅𝑠OLD⁡Uy∈X
9 8 adantrl ⊢U∈NrmCVec∧x∈X∧y∈X→-1⋅𝑠OLD⁡Uy∈X
10 eqid ⊢+v⁡U=+v⁡U
11 1 10 nvgcl ⊢U∈NrmCVec∧x∈X∧-1⋅𝑠OLD⁡Uy∈X→x+v⁡U-1⋅𝑠OLD⁡Uy∈X
12 3 4 9 11 syl3anc ⊢U∈NrmCVec∧x∈X∧y∈X→x+v⁡U-1⋅𝑠OLD⁡Uy∈X
13 12 ralrimivva ⊢U∈NrmCVec→∀x∈X∀y∈Xx+v⁡U-1⋅𝑠OLD⁡Uy∈X
14 eqid ⊢x∈X,y∈X⟼x+v⁡U-1⋅𝑠OLD⁡Uy=x∈X,y∈X⟼x+v⁡U-1⋅𝑠OLD⁡Uy
15 14 fmpo ⊢∀x∈X∀y∈Xx+v⁡U-1⋅𝑠OLD⁡Uy∈X↔x∈X,y∈X⟼x+v⁡U-1⋅𝑠OLD⁡Uy:X×X⟶X
16 13 15 sylib ⊢U∈NrmCVec→x∈X,y∈X⟼x+v⁡U-1⋅𝑠OLD⁡Uy:X×X⟶X
17 1 10 6 2 nvmfval ⊢U∈NrmCVec→M=x∈X,y∈X⟼x+v⁡U-1⋅𝑠OLD⁡Uy
18 17 feq1d ⊢U∈NrmCVec→M:X×X⟶X↔x∈X,y∈X⟼x+v⁡U-1⋅𝑠OLD⁡Uy:X×X⟶X
19 16 18 mpbird ⊢U∈NrmCVec→M:X×X⟶X