Theorem matgrp

Description: The matrix ring is a group. (Contributed by AV, 21-Dec-2019)

	Ref	Expression
Hypothesis	matlmod.a	|- A = ( N Mat R )
Assertion	matgrp	|- ( ( N e. Fin /\ R e. Ring ) -> A e. Grp )

Proof

Step	Hyp	Ref	Expression
1		matlmod.a	|- A = ( N Mat R )
2	1	matlmod	|- ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
3		lmodgrp	|- ( A e. LMod -> A e. Grp )
4	2 3	syl	|- ( ( N e. Fin /\ R e. Ring ) -> A e. Grp )