Definition df-dmatalt

Description: Define the set of n x n diagonal (square) matrices over a set (usually a ring) r, see definition in Roman p. 4 or Definition 3.12 in Hefferon p. 240. (Contributed by AV, 8-Dec-2019)

	Ref	Expression
Assertion	df-dmatalt	⊢ DMatALT = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmatalt	⊢ DMatALT
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		vi	⊢ 𝑖
16		vj	⊢ 𝑗
17	15	cv	⊢ 𝑖
18	16	cv	⊢ 𝑗
19	17 18	wne	⊢ 𝑖 ≠ 𝑗
20	12	cv	⊢ 𝑚
21	17 18 20	co	⊢ ( 𝑖 𝑚 𝑗 )
22		c0g	⊢ 0g
23	7 22	cfv	⊢ ( 0g ‘ 𝑟 )
24	21 23	wceq	⊢ ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 )
25	19 24	wi	⊢ ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) )
26	25 16 5	wral	⊢ ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) )
27	26 15 5	wral	⊢ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) )
28	27 12 14	crab	⊢ { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) }
29	10 28 11	co	⊢ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } )
30	9 8 29	csb	⊢ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } )
31	1 3 2 4 30	cmpo	⊢ ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) )
32	0 31	wceq	⊢ DMatALT = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) )