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 Mat R$
	matbas.g	$⊢ G = R freeLMod (N \times N)$
Assertion	matinvg	$⊢ (N \in Fin \land R \in V) \to {inv}_{g} (G) = {inv}_{g} (A)$

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

Metamath Proof Explorer