Theorem matgrp

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

	Ref	Expression
Hypothesis	matlmod.a	$$⊢A=N\mathrm{Mat}R$$
Assertion	matgrp	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to A\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		matlmod.a	$$⊢A=N\mathrm{Mat}R$$
2	1	matlmod	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to A\in \mathrm{LMod}$$
3		lmodgrp	$$⊢A\in \mathrm{LMod}\to A\in \mathrm{Grp}$$
4	2 3	syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to A\in \mathrm{Grp}$$