Theorem dmatALTval

Description: The algebra of N x N diagonal matrices over a ring R . (Contributed by AV, 8-Dec-2019)

	Ref	Expression
Hypotheses	dmatALTval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	dmatALTval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	dmatALTval.0	⊢ 0 = ( 0g ‘ 𝑅 )
	dmatALTval.d	⊢ 𝐷 = ( 𝑁 DMatALT 𝑅 )
Assertion	dmatALTval	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → 𝐷 = ( 𝐴 ↾s { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		dmatALTval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		dmatALTval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		dmatALTval.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		dmatALTval.d	⊢ 𝐷 = ( 𝑁 DMatALT 𝑅 )
5		ovexd	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) ∈ V )
6		id	⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → 𝑎 = ( 𝑛 Mat 𝑟 ) )
7		fveq2	⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( Base ‘ 𝑎 ) = ( Base ‘ ( 𝑛 Mat 𝑟 ) ) )
8	7	rabeqdv	⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } = { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } )
9	6 8	oveq12d	⊢ ( 𝑎 = ( 𝑛 Mat 𝑟 ) → ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) = ( ( 𝑛 Mat 𝑟 ) ↾s { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) )
10	9	adantl	⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ∧ 𝑎 = ( 𝑛 Mat 𝑟 ) ) → ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) = ( ( 𝑛 Mat 𝑟 ) ↾s { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) )
11	5 10	csbied	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) = ( ( 𝑛 Mat 𝑟 ) ↾s { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) )
12		oveq12	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
13	12 1	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = 𝐴 )
14	13	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = ( Base ‘ 𝐴 ) )
15	14 2	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = 𝐵 )
16		simpl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
17		fveq2	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
18	17 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
19	18	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 0g ‘ 𝑟 ) = 0 )
20	19	eqeq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ↔ ( 𝑖 𝑚 𝑗 ) = 0 ) )
21	20	imbi2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) ↔ ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
22	16 21	raleqbidv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) ↔ ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
23	16 22	raleqbidv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
24	15 23	rabeqbidv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
25	13 24	oveq12d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( 𝑛 Mat 𝑟 ) ↾s { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) = ( 𝐴 ↾s { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ) )
26	11 25	eqtrd	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) = ( 𝐴 ↾s { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ) )
27		df-dmatalt	⊢ DMatALT = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ ⦋ ( 𝑛 Mat 𝑟 ) / 𝑎 ⦌ ( 𝑎 ↾s { 𝑚 ∈ ( Base ‘ 𝑎 ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) )
28		ovex	⊢ ( 𝐴 ↾s { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ) ∈ V
29	26 27 28	ovmpoa	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑁 DMatALT 𝑅 ) = ( 𝐴 ↾s { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ) )
30	4 29	syl5eq	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → 𝐷 = ( 𝐴 ↾s { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ) )