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 Mat R )
	matbas.g	|- G = ( R freeLMod ( N X. N ) )
Assertion	matinvg	|- ( ( N e. Fin /\ R e. V ) -> ( invg ` G ) = ( invg ` A ) )

Proof

Step	Hyp	Ref	Expression
1		matbas.a	|- A = ( N Mat R )
2		matbas.g	|- G = ( R freeLMod ( N X. N ) )
3		eqidd	|- ( ( N e. Fin /\ R e. V ) -> ( Base ` G ) = ( Base ` G ) )
4	1 2	matbas	|- ( ( N e. Fin /\ R e. V ) -> ( Base ` G ) = ( Base ` A ) )
5	1 2	matplusg	|- ( ( N e. Fin /\ R e. V ) -> ( +g ` G ) = ( +g ` A ) )
6	5	oveqdr	|- ( ( ( N e. Fin /\ R e. V ) /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x ( +g ` A ) y ) )
7	3 4 6	grpinvpropd	|- ( ( N e. Fin /\ R e. V ) -> ( invg ` G ) = ( invg ` A ) )