Definition df-scmat

Description: Define the algebra of n x n scalar matrices over a set (usually a ring) r, see definition in Connell p. 57: "Ascalar matrix is a diagonal matrix for which all the diagonal terms are equal, i.e., a matrix of the form cI_n". (Contributed by AV, 8-Dec-2019)

	Ref	Expression
Assertion	df-scmat	⊢ ScMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cscmat	⊢ ScMat
1		vn	⊢ 𝑛
2		cfn	⊢ Fin
3		vr	⊢ 𝑟
4		cvv	⊢ V
5	1	cv	⊢ 𝑛
6		cmat	⊢ Mat
7	3	cv	⊢ 𝑟
8	5 7 6	co	⊢ ( 𝑛 Mat 𝑟 )
9		va	⊢ 𝑎
10		vm	⊢ 𝑚
11		cbs	⊢ Base
12	9	cv	⊢ 𝑎
13	12 11	cfv	⊢ ( Base ‘ 𝑎 )
14		vc	⊢ 𝑐
15	7 11	cfv	⊢ ( Base ‘ 𝑟 )
16	10	cv	⊢ 𝑚
17	14	cv	⊢ 𝑐
18		cvsca	⊢ ·𝑠
19	12 18	cfv	⊢ ( ·𝑠 ‘ 𝑎 )
20		cur	⊢ 1r
21	12 20	cfv	⊢ ( 1r ‘ 𝑎 )
22	17 21 19	co	⊢ ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) )
23	16 22	wceq	⊢ 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) )
24	23 14 15	wrex	⊢ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) )
25	24 10 13	crab	⊢ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) }
26	9 8 25	csb	⊢ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) }
27	1 3 2 4 26	cmpo	⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) } )
28	0 27	wceq	⊢ ScMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) 𝑚 = ( 𝑐 ( ·𝑠 ‘ 𝑎 ) ( 1r ‘ 𝑎 ) ) } )