Theorem dmatval

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

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

Proof

Step	Hyp	Ref	Expression
1		dmatval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		dmatval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		dmatval.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		dmatval.d	⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
5		df-dmat	⊢ DMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } )
6	5	a1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → DMat = ( 𝑛 ∈ Fin , 𝑟 ∈ V ↦ { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } ) )
7		oveq12	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
8	7	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) ) )
9	1	fveq2i	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
10	2 9	eqtri	⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
11	8 10	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = 𝐵 )
12		simpl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
13		fveq2	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
14	13 3	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
15	14	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 0g ‘ 𝑟 ) = 0 )
16	15	eqeq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ↔ ( 𝑖 𝑚 𝑗 ) = 0 ) )
17	16	imbi2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) ↔ ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
18	12 17	raleqbidv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) ↔ ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
19	12 18	raleqbidv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) ) )
20	11 19	rabeqbidv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
21	20	adantl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) ∧ ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) ) → { 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ∣ ∀ 𝑖 ∈ 𝑛 ∀ 𝑗 ∈ 𝑛 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = ( 0g ‘ 𝑟 ) ) } = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
22		simpl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑁 ∈ Fin )
23		elex	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
24	23	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝑅 ∈ V )
25	2	fvexi	⊢ 𝐵 ∈ V
26		rabexg	⊢ ( 𝐵 ∈ V → { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ∈ V )
27	25 26	mp1i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } ∈ V )
28	6 21 22 24 27	ovmpod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑁 DMat 𝑅 ) = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )
29	4 28	syl5eq	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → 𝐷 = { 𝑚 ∈ 𝐵 ∣ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ≠ 𝑗 → ( 𝑖 𝑚 𝑗 ) = 0 ) } )