Theorem dmatsgrp

Description: The set of diagonal matrices is a subgroup of the matrix group/algebra. (Contributed by AV, 19-Aug-2019) (Revised by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	dmatid.a	|- A = ( N Mat R )
	dmatid.b	|- B = ( Base ` A )
	dmatid.0	|- .0. = ( 0g ` R )
	dmatid.d	|- D = ( N DMat R )
Assertion	dmatsgrp	|- ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubGrp ` A ) )

Proof

Step	Hyp	Ref	Expression
1		dmatid.a	|- A = ( N Mat R )
2		dmatid.b	|- B = ( Base ` A )
3		dmatid.0	|- .0. = ( 0g ` R )
4		dmatid.d	|- D = ( N DMat R )
5	1 2 3 4	dmatmat	|- ( ( N e. Fin /\ R e. Ring ) -> ( z e. D -> z e. B ) )
6	5	ancoms	|- ( ( R e. Ring /\ N e. Fin ) -> ( z e. D -> z e. B ) )
7	6	ssrdv	|- ( ( R e. Ring /\ N e. Fin ) -> D C_ B )
8	1 2 3 4	dmatid	|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. D )
9	8	ancoms	|- ( ( R e. Ring /\ N e. Fin ) -> ( 1r ` A ) e. D )
10	9	ne0d	|- ( ( R e. Ring /\ N e. Fin ) -> D =/= (/) )
11	1 2 3 4	dmatsubcl	|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. D /\ y e. D ) ) -> ( x ( -g ` A ) y ) e. D )
12	11	ancom1s	|- ( ( ( R e. Ring /\ N e. Fin ) /\ ( x e. D /\ y e. D ) ) -> ( x ( -g ` A ) y ) e. D )
13	12	ralrimivva	|- ( ( R e. Ring /\ N e. Fin ) -> A. x e. D A. y e. D ( x ( -g ` A ) y ) e. D )
14	1	matring	|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
15	14	ancoms	|- ( ( R e. Ring /\ N e. Fin ) -> A e. Ring )
16		ringgrp	|- ( A e. Ring -> A e. Grp )
17		eqid	|- ( -g ` A ) = ( -g ` A )
18	2 17	issubg4	|- ( A e. Grp -> ( D e. ( SubGrp ` A ) <-> ( D C_ B /\ D =/= (/) /\ A. x e. D A. y e. D ( x ( -g ` A ) y ) e. D ) ) )
19	15 16 18	3syl	|- ( ( R e. Ring /\ N e. Fin ) -> ( D e. ( SubGrp ` A ) <-> ( D C_ B /\ D =/= (/) /\ A. x e. D A. y e. D ( x ( -g ` A ) y ) e. D ) ) )
20	7 10 13 19	mpbir3and	|- ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubGrp ` A ) )