# Metamath Proof Explorer

## Theorem nvinv

Description: Minus 1 times a vector is the underlying group's inverse element. Equation 2 of Kreyszig p. 51. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 nvinv.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nvinv.2 ${⊢}{G}={+}_{v}\left({U}\right)$
3 nvinv.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
4 nvinv.5 ${⊢}{M}=\mathrm{inv}\left({G}\right)$
5 eqid ${⊢}{1}^{st}\left({U}\right)={1}^{st}\left({U}\right)$
6 5 nvvc ${⊢}{U}\in \mathrm{NrmCVec}\to {1}^{st}\left({U}\right)\in {CVec}_{\mathrm{OLD}}$
7 2 vafval ${⊢}{G}={1}^{st}\left({1}^{st}\left({U}\right)\right)$
8 3 smfval ${⊢}{S}={2}^{nd}\left({1}^{st}\left({U}\right)\right)$
9 1 2 bafval ${⊢}{X}=\mathrm{ran}{G}$
10 7 8 9 4 vcm ${⊢}\left({1}^{st}\left({U}\right)\in {CVec}_{\mathrm{OLD}}\wedge {A}\in {X}\right)\to -1{S}{A}={M}\left({A}\right)$
11 6 10 sylan ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in {X}\right)\to -1{S}{A}={M}\left({A}\right)$