Theorem dmatALTbas

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

	Ref	Expression
Hypotheses	dmatALTval.a	|- A = ( N Mat R )
	dmatALTval.b	|- B = ( Base ` A )
	dmatALTval.0	|- .0. = ( 0g ` R )
	dmatALTval.d	|- D = ( N DMatALT R )
Assertion	dmatALTbas	|- ( ( N e. Fin /\ R e. _V ) -> ( Base ` D ) = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )

Proof

Step	Hyp	Ref	Expression
1		dmatALTval.a	|- A = ( N Mat R )
2		dmatALTval.b	|- B = ( Base ` A )
3		dmatALTval.0	|- .0. = ( 0g ` R )
4		dmatALTval.d	|- D = ( N DMatALT R )
5	1 2 3 4	dmatALTval	|- ( ( N e. Fin /\ R e. _V ) -> D = ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) )
6	5	fveq2d	|- ( ( N e. Fin /\ R e. _V ) -> ( Base ` D ) = ( Base ` ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) ) )
7	2	fvexi	|- B e. _V
8		rabexg	|- ( B e. _V -> { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } e. _V )
9	7 8	mp1i	|- ( ( N e. Fin /\ R e. _V ) -> { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } e. _V )
10		eqid	|- ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) = ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
11	10 2	ressbas	|- ( { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } e. _V -> ( { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } i^i B ) = ( Base ` ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) ) )
12	9 11	syl	|- ( ( N e. Fin /\ R e. _V ) -> ( { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } i^i B ) = ( Base ` ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } ) ) )
13		inrab2	|- ( { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } i^i B ) = { m e. ( B i^i B ) | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) }
14		inidm	|- ( B i^i B ) = B
15		rabeq	|- ( ( B i^i B ) = B -> { m e. ( B i^i B ) | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
16	14 15	mp1i	|- ( ( N e. Fin /\ R e. _V ) -> { m e. ( B i^i B ) | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
17	13 16	syl5eq	|- ( ( N e. Fin /\ R e. _V ) -> ( { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } i^i B ) = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
18	6 12 17	3eqtr2d	|- ( ( N e. Fin /\ R e. _V ) -> ( Base ` D ) = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )