Metamath Proof Explorer

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 ⊢A=NMatR
dmatALTval.b ⊢B=BaseA
dmatALTval.0 ⊢0˙=0R
dmatALTval.d ⊢D=NDMatALTR
Assertion dmatALTval ⊢N∈Fin∧R∈V→D=A↾𝑠m∈B|∀i∈N∀j∈Ni≠j→imj=0˙

Proof

Step Hyp Ref Expression
1 dmatALTval.a ⊢A=NMatR
2 dmatALTval.b ⊢B=BaseA
3 dmatALTval.0 ⊢0˙=0R
4 dmatALTval.d ⊢D=NDMatALTR
5 ovexd ⊢n=N∧r=R→nMatr∈V
6 id ⊢a=nMatr→a=nMatr
7 fveq2 ⊢a=nMatr→Basea=BasenMatr
8 7 rabeqdv ⊢a=nMatr→m∈Basea|∀i∈n∀j∈ni≠j→imj=0r=m∈BasenMatr|∀i∈n∀j∈ni≠j→imj=0r
9 6 8 oveq12d ⊢a=nMatr→a↾𝑠m∈Basea|∀i∈n∀j∈ni≠j→imj=0r=nMatr↾𝑠m∈BasenMatr|∀i∈n∀j∈ni≠j→imj=0r
10 9 adantl ⊢n=N∧r=R∧a=nMatr→a↾𝑠m∈Basea|∀i∈n∀j∈ni≠j→imj=0r=nMatr↾𝑠m∈BasenMatr|∀i∈n∀j∈ni≠j→imj=0r
11 5 10 csbied ⊢n=N∧r=R→⦋nMatr/a⦌a↾𝑠m∈Basea|∀i∈n∀j∈ni≠j→imj=0r=nMatr↾𝑠m∈BasenMatr|∀i∈n∀j∈ni≠j→imj=0r
12 oveq12 ⊢n=N∧r=R→nMatr=NMatR
13 12 1 eqtr4di ⊢n=N∧r=R→nMatr=A
14 13 fveq2d ⊢n=N∧r=R→BasenMatr=BaseA
15 14 2 eqtr4di ⊢n=N∧r=R→BasenMatr=B
16 simpl ⊢n=N∧r=R→n=N
17 fveq2 ⊢r=R→0r=0R
18 17 3 eqtr4di ⊢r=R→0r=0˙
19 18 adantl ⊢n=N∧r=R→0r=0˙
20 19 eqeq2d ⊢n=N∧r=R→imj=0r↔imj=0˙
21 20 imbi2d ⊢n=N∧r=R→i≠j→imj=0r↔i≠j→imj=0˙
22 16 21 raleqbidv ⊢n=N∧r=R→∀j∈ni≠j→imj=0r↔∀j∈Ni≠j→imj=0˙
23 16 22 raleqbidv ⊢n=N∧r=R→∀i∈n∀j∈ni≠j→imj=0r↔∀i∈N∀j∈Ni≠j→imj=0˙
24 15 23 rabeqbidv ⊢n=N∧r=R→m∈BasenMatr|∀i∈n∀j∈ni≠j→imj=0r=m∈B|∀i∈N∀j∈Ni≠j→imj=0˙
25 13 24 oveq12d ⊢n=N∧r=R→nMatr↾𝑠m∈BasenMatr|∀i∈n∀j∈ni≠j→imj=0r=A↾𝑠m∈B|∀i∈N∀j∈Ni≠j→imj=0˙
26 11 25 eqtrd ⊢n=N∧r=R→⦋nMatr/a⦌a↾𝑠m∈Basea|∀i∈n∀j∈ni≠j→imj=0r=A↾𝑠m∈B|∀i∈N∀j∈Ni≠j→imj=0˙
27 df-dmatalt ⊢DMatALT=n∈Fin,r∈V⟼⦋nMatr/a⦌a↾𝑠m∈Basea|∀i∈n∀j∈ni≠j→imj=0r
28 ovex ⊢A↾𝑠m∈B|∀i∈N∀j∈Ni≠j→imj=0˙∈V
29 26 27 28 ovmpoa ⊢N∈Fin∧R∈V→NDMatALTR=A↾𝑠m∈B|∀i∈N∀j∈Ni≠j→imj=0˙
30 4 29 eqtrid ⊢N∈Fin∧R∈V→D=A↾𝑠m∈B|∀i∈N∀j∈Ni≠j→imj=0˙