Theorem matsubg

Description: The matrix ring has the same addition as its underlying group. (Contributed by AV, 2-Aug-2019)

	Ref	Expression
Hypotheses	matsubg.a	|- A = ( N Mat R )
	matsubg.g	|- G = ( R freeLMod ( N X. N ) )
Assertion	matsubg	|- ( ( N e. Fin /\ R e. V ) -> ( -g ` G ) = ( -g ` A ) )

Proof

Step	Hyp	Ref	Expression
1		matsubg.a	|- A = ( N Mat R )
2		matsubg.g	|- G = ( R freeLMod ( N X. N ) )
3	1 2	matbas	|- ( ( N e. Fin /\ R e. V ) -> ( Base ` G ) = ( Base ` A ) )
4	1 2	matplusg	|- ( ( N e. Fin /\ R e. V ) -> ( +g ` G ) = ( +g ` A ) )
5	3 4	grpsubpropd	|- ( ( N e. Fin /\ R e. V ) -> ( -g ` G ) = ( -g ` A ) )