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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatstrbas.c	⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
	scmatstrbas.s	⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
Assertion	scmatstrbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑆 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		scmatstrbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		scmatstrbas.c	⊢ 𝐶 = ( 𝑁 ScMat 𝑅 )
3		scmatstrbas.s	⊢ 𝑆 = ( 𝐴 ↾s 𝐶 )
4		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7	1 4 5 6 2	scmatsrng	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ ( SubRing ‘ 𝐴 ) )
8	3	subrgbas	⊢ ( 𝐶 ∈ ( SubRing ‘ 𝐴 ) → 𝐶 = ( Base ‘ 𝑆 ) )
9	8	eqcomd	⊢ ( 𝐶 ∈ ( SubRing ‘ 𝐴 ) → ( Base ‘ 𝑆 ) = 𝐶 )
10	7 9	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑆 ) = 𝐶 )