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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matsubg.g	⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
Assertion	matsubg	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( -g ‘ 𝐺 ) = ( -g ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		matsubg.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matsubg.g	⊢ 𝐺 = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
3	1 2	matbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐴 ) )
4	1 2	matplusg	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐴 ) )
5	3 4	grpsubpropd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( -g ‘ 𝐺 ) = ( -g ‘ 𝐴 ) )