# Metamath Proof Explorer

## Theorem nvmval

Description: Value of vector subtraction on a normed complex vector space. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvmval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nvmval.2 ${⊢}{G}={+}_{v}\left({U}\right)$
nvmval.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
nvmval.3 ${⊢}{M}={-}_{v}\left({U}\right)$
Assertion nvmval ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{M}{B}={A}{G}\left(-1{S}{B}\right)$

### Proof

Step Hyp Ref Expression
1 nvmval.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nvmval.2 ${⊢}{G}={+}_{v}\left({U}\right)$
3 nvmval.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
4 nvmval.3 ${⊢}{M}={-}_{v}\left({U}\right)$
5 2 nvgrp ${⊢}{U}\in \mathrm{NrmCVec}\to {G}\in \mathrm{GrpOp}$
6 1 2 bafval ${⊢}{X}=\mathrm{ran}{G}$
7 eqid ${⊢}\mathrm{inv}\left({G}\right)=\mathrm{inv}\left({G}\right)$
8 eqid ${⊢}{/}_{g}\left({G}\right)={/}_{g}\left({G}\right)$
9 6 7 8 grpodivval ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{/}_{g}\left({G}\right){B}={A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)$
10 5 9 syl3an1 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{/}_{g}\left({G}\right){B}={A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)$
11 1 2 4 8 nvm ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{M}{B}={A}{/}_{g}\left({G}\right){B}$
12 1 2 3 7 nvinv ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to -1{S}{B}=\mathrm{inv}\left({G}\right)\left({B}\right)$
13 12 3adant2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to -1{S}{B}=\mathrm{inv}\left({G}\right)\left({B}\right)$
14 13 oveq2d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}\left(-1{S}{B}\right)={A}{G}\mathrm{inv}\left({G}\right)\left({B}\right)$
15 10 11 14 3eqtr4d ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{M}{B}={A}{G}\left(-1{S}{B}\right)$