Theorem scmatstrbas

Description: The set of scalar matrices is the base set of the ring of corresponding scalar matrices. (Contributed by AV, 26-Dec-2019)

	Ref	Expression
Hypotheses	scmatstrbas.a	|- A = ( N Mat R )
	scmatstrbas.c	|- C = ( N ScMat R )
	scmatstrbas.s	|- S = ( A |`s C )
Assertion	scmatstrbas	|- ( ( N e. Fin /\ R e. Ring ) -> ( Base ` S ) = C )

Proof

Step	Hyp	Ref	Expression
1		scmatstrbas.a	|- A = ( N Mat R )
2		scmatstrbas.c	|- C = ( N ScMat R )
3		scmatstrbas.s	|- S = ( A |`s C )
4		eqid	|- ( Base ` A ) = ( Base ` A )
5		eqid	|- ( Base ` R ) = ( Base ` R )
6		eqid	|- ( 0g ` R ) = ( 0g ` R )
7	1 4 5 6 2	scmatsrng	|- ( ( N e. Fin /\ R e. Ring ) -> C e. ( SubRing ` A ) )
8	3	subrgbas	|- ( C e. ( SubRing ` A ) -> C = ( Base ` S ) )
9	8	eqcomd	|- ( C e. ( SubRing ` A ) -> ( Base ` S ) = C )
10	7 9	syl	|- ( ( N e. Fin /\ R e. Ring ) -> ( Base ` S ) = C )