# 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}=\mathrm{BaseSet}\left({U}\right)$
nvmf.3 ${⊢}{M}={-}_{v}\left({U}\right)$
Assertion nvmf ${⊢}{U}\in \mathrm{NrmCVec}\to {M}:{X}×{X}⟶{X}$

### Proof

Step Hyp Ref Expression
1 nvmf.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nvmf.3 ${⊢}{M}={-}_{v}\left({U}\right)$
3 simpl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {U}\in \mathrm{NrmCVec}$
4 simprl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}\in {X}$
5 neg1cn ${⊢}-1\in ℂ$
6 eqid ${⊢}{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
7 1 6 nvscl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge -1\in ℂ\wedge {y}\in {X}\right)\to -1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\in {X}$
8 5 7 mp3an2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {y}\in {X}\right)\to -1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\in {X}$
9 8 adantrl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to -1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\in {X}$
10 eqid ${⊢}{+}_{v}\left({U}\right)={+}_{v}\left({U}\right)$
11 1 10 nvgcl ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {x}\in {X}\wedge -1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\in {X}\right)\to {x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\in {X}$
12 3 4 9 11 syl3anc ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({x}\in {X}\wedge {y}\in {X}\right)\right)\to {x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\in {X}$
13 12 ralrimivva ${⊢}{U}\in \mathrm{NrmCVec}\to \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\in {X}$
14 eqid ${⊢}\left({x}\in {X},{y}\in {X}⟼{x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\right)=\left({x}\in {X},{y}\in {X}⟼{x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\right)$
15 14 fmpo ${⊢}\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\in {X}↔\left({x}\in {X},{y}\in {X}⟼{x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\right):{X}×{X}⟶{X}$
16 13 15 sylib ${⊢}{U}\in \mathrm{NrmCVec}\to \left({x}\in {X},{y}\in {X}⟼{x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\right):{X}×{X}⟶{X}$
17 1 10 6 2 nvmfval ${⊢}{U}\in \mathrm{NrmCVec}\to {M}=\left({x}\in {X},{y}\in {X}⟼{x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\right)$
18 17 feq1d ${⊢}{U}\in \mathrm{NrmCVec}\to \left({M}:{X}×{X}⟶{X}↔\left({x}\in {X},{y}\in {X}⟼{x}{+}_{v}\left({U}\right)\left(-1{\cdot }_{\mathrm{𝑠OLD}}\left({U}\right){y}\right)\right):{X}×{X}⟶{X}\right)$
19 16 18 mpbird ${⊢}{U}\in \mathrm{NrmCVec}\to {M}:{X}×{X}⟶{X}$