Metamath Proof Explorer


Theorem matgrp

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

Ref Expression
Hypothesis matlmod.a 𝐴 = ( 𝑁 Mat 𝑅 )
Assertion matgrp ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp )

Proof

Step Hyp Ref Expression
1 matlmod.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 1 matlmod ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
3 lmodgrp ( 𝐴 ∈ LMod → 𝐴 ∈ Grp )
4 2 3 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp )