Definition df-scmatalt

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-scmatalt	⊢ ScMatALT = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cscmatalt	⊢ ScMatALT
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	9	cv	⊢ 𝑎
11		cress	⊢ ↾s
12		vm	⊢ 𝑚
13		cbs	⊢ Base
14	10 13	cfv	⊢ ( Base ‘ 𝑎 )
15		vc	⊢ 𝑐
16	7 13	cfv	⊢ ( Base ‘ 𝑟 )
17		vi	⊢ 𝑖
18		vj	⊢ 𝑗
19	17	cv	⊢ 𝑖
20	12	cv	⊢ 𝑚
21	18	cv	⊢ 𝑗
22	19 21 20	co	⊢ ( 𝑖 𝑚 𝑗 )
23	19 21	wceq	⊢ 𝑖 = 𝑗
24	15	cv	⊢ 𝑐
25		c0g	⊢ 0g
26	7 25	cfv	⊢ ( 0g ‘ 𝑟 )
27	23 24 26	cif	⊢ if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) )
28	22 27	wceq	⊢ ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) )
29	28 18 5	wral	⊢ ∀ 𝑗 ∈ 𝑛 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) )
30	29 17 5	wral	⊢ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) )
31	30 15 16	wrex	⊢ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) )
32	31 12 14	crab	⊢ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) ) }
33	10 32 11	co	⊢ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) ) } )
34	9 8 33	csb	⊢ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) ) } )
35	1 3 2 4 34	cmpo	⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) ) } ) )
36	0 35	wceq	⊢ ScMatALT = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∃ 𝑐 ∈ ( Base ‘ 𝑟 ) ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 𝑚 𝑗 ) = if ( 𝑖 = 𝑗 , 𝑐 , ( 0g ‘ 𝑟 ) ) } ) )