# Metamath Proof Explorer

## Theorem matinvg

Description: The matrix ring has the same additive inverse as its underlying linear structure. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypotheses matbas.a ${⊢}{A}={N}\mathrm{Mat}{R}$
matbas.g ${⊢}{G}={R}\mathrm{freeLMod}\left({N}×{N}\right)$
Assertion matinvg ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {inv}_{g}\left({G}\right)={inv}_{g}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 matbas.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 matbas.g ${⊢}{G}={R}\mathrm{freeLMod}\left({N}×{N}\right)$
3 eqidd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{G}}$
4 1 2 matbas ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {\mathrm{Base}}_{{G}}={\mathrm{Base}}_{{A}}$
5 1 2 matplusg ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {+}_{{G}}={+}_{{A}}$
6 5 oveqdr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\wedge \left({x}\in {\mathrm{Base}}_{{G}}\wedge {y}\in {\mathrm{Base}}_{{G}}\right)\right)\to {x}{+}_{{G}}{y}={x}{+}_{{A}}{y}$
7 3 4 6 grpinvpropd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {inv}_{g}\left({G}\right)={inv}_{g}\left({A}\right)$