Theorem dmatbas

Description: The set of all N x N diagonal matrices over (the ring) R is the base set of the algebra of N x N diagonal matrices over (the ring) R . (Contributed by AV, 8-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dmatbas.a	|- A = ( N Mat R )
2		dmatbas.b	|- B = ( Base ` A )
3		dmatbas.0	|- .0. = ( 0g ` R )
4		dmatbas.d	|- D = ( N DMat R )
5	1 2 3 4	dmatval	|- ( ( N e. Fin /\ R e. V ) -> D = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
6		elex	|- ( R e. V -> R e. _V )
7		eqid	|- ( N DMatALT R ) = ( N DMatALT R )
8	1 2 3 7	dmatALTbas	|- ( ( N e. Fin /\ R e. _V ) -> ( Base ` ( N DMatALT R ) ) = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
9	6 8	sylan2	|- ( ( N e. Fin /\ R e. V ) -> ( Base ` ( N DMatALT R ) ) = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
10	5 9	eqtr4d	|- ( ( N e. Fin /\ R e. V ) -> D = ( Base ` ( N DMatALT R ) ) )