Metamath Proof Explorer


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 A = N Mat R
dmatval.b B = Base A
dmatval.0 0 ˙ = 0 R
dmatval.d D = N DMat R
Assertion dmatval N Fin R V D = m B | i N j N i j i m j = 0 ˙

Proof

Step Hyp Ref Expression
1 dmatval.a A = N Mat R
2 dmatval.b B = Base A
3 dmatval.0 0 ˙ = 0 R
4 dmatval.d D = N DMat R
5 df-dmat DMat = n Fin , r V m Base n Mat r | i n j n i j i m j = 0 r
6 5 a1i N Fin R V DMat = n Fin , r V m Base n Mat r | i n j n i j i m j = 0 r
7 oveq12 n = N r = R n Mat r = N Mat R
8 7 fveq2d n = N r = R Base n Mat r = Base N Mat R
9 1 fveq2i Base A = Base N Mat R
10 2 9 eqtri B = Base N Mat R
11 8 10 eqtr4di n = N r = R Base n Mat r = B
12 simpl n = N r = R n = N
13 fveq2 r = R 0 r = 0 R
14 13 3 eqtr4di r = R 0 r = 0 ˙
15 14 adantl n = N r = R 0 r = 0 ˙
16 15 eqeq2d n = N r = R i m j = 0 r i m j = 0 ˙
17 16 imbi2d n = N r = R i j i m j = 0 r i j i m j = 0 ˙
18 12 17 raleqbidv n = N r = R j n i j i m j = 0 r j N i j i m j = 0 ˙
19 12 18 raleqbidv n = N r = R i n j n i j i m j = 0 r i N j N i j i m j = 0 ˙
20 11 19 rabeqbidv n = N r = R m Base n Mat r | i n j n i j i m j = 0 r = m B | i N j N i j i m j = 0 ˙
21 20 adantl N Fin R V n = N r = R m Base n Mat r | i n j n i j i m j = 0 r = m B | i N j N i j i m j = 0 ˙
22 simpl N Fin R V N Fin
23 elex R V R V
24 23 adantl N Fin R V R V
25 2 fvexi B V
26 rabexg B V m B | i N j N i j i m j = 0 ˙ V
27 25 26 mp1i N Fin R V m B | i N j N i j i m j = 0 ˙ V
28 6 21 22 24 27 ovmpod N Fin R V N DMat R = m B | i N j N i j i m j = 0 ˙
29 4 28 syl5eq N Fin R V D = m B | i N j N i j i m j = 0 ˙