Metamath Proof Explorer

Theorem scmatdmat

Description: A scalar matrix is a diagonal matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 19-Dec-2019)

Ref Expression
Hypotheses scmatid.a ⊢A=NMatR
scmatid.b ⊢B=BaseA
scmatid.e ⊢E=BaseR
scmatid.0 ⊢0˙=0R
scmatid.s ⊢S=NScMatR
scmatdmat.d ⊢D=NDMatR
Assertion scmatdmat ⊢N∈Fin∧R∈Ring→M∈S→M∈D

Proof

Step Hyp Ref Expression
1 scmatid.a ⊢A=NMatR
2 scmatid.b ⊢B=BaseA
3 scmatid.e ⊢E=BaseR
4 scmatid.0 ⊢0˙=0R
5 scmatid.s ⊢S=NScMatR
6 scmatdmat.d ⊢D=NDMatR
7 id ⊢imj=ifi=jc0˙→imj=ifi=jc0˙
8 ifnefalse ⊢i≠j→ifi=jc0˙=0˙
9 7 8 sylan9eq ⊢imj=ifi=jc0˙∧i≠j→imj=0˙
10 9 ex ⊢imj=ifi=jc0˙→i≠j→imj=0˙
11 10 a1i ⊢N∈Fin∧R∈Ring∧m∈B∧c∈E∧i∈N∧j∈N→imj=ifi=jc0˙→i≠j→imj=0˙
12 11 ralimdva ⊢N∈Fin∧R∈Ring∧m∈B∧c∈E∧i∈N→∀j∈Nimj=ifi=jc0˙→∀j∈Ni≠j→imj=0˙
13 12 ralimdva ⊢N∈Fin∧R∈Ring∧m∈B∧c∈E→∀i∈N∀j∈Nimj=ifi=jc0˙→∀i∈N∀j∈Ni≠j→imj=0˙
14 13 rexlimdva ⊢N∈Fin∧R∈Ring∧m∈B→∃c∈E∀i∈N∀j∈Nimj=ifi=jc0˙→∀i∈N∀j∈Ni≠j→imj=0˙
15 14 ss2rabdv ⊢N∈Fin∧R∈Ring→m∈B|∃c∈E∀i∈N∀j∈Nimj=ifi=jc0˙⊆m∈B|∀i∈N∀j∈Ni≠j→imj=0˙
16 15 adantr ⊢N∈Fin∧R∈Ring∧M∈S→m∈B|∃c∈E∀i∈N∀j∈Nimj=ifi=jc0˙⊆m∈B|∀i∈N∀j∈Ni≠j→imj=0˙
17 1 2 5 3 4 scmatmats ⊢N∈Fin∧R∈Ring→S=m∈B|∃c∈E∀i∈N∀j∈Nimj=ifi=jc0˙
18 1 2 4 6 dmatval ⊢N∈Fin∧R∈Ring→D=m∈B|∀i∈N∀j∈Ni≠j→imj=0˙
19 17 18 sseq12d ⊢N∈Fin∧R∈Ring→S⊆D↔m∈B|∃c∈E∀i∈N∀j∈Nimj=ifi=jc0˙⊆m∈B|∀i∈N∀j∈Ni≠j→imj=0˙
20 19 adantr ⊢N∈Fin∧R∈Ring∧M∈S→S⊆D↔m∈B|∃c∈E∀i∈N∀j∈Nimj=ifi=jc0˙⊆m∈B|∀i∈N∀j∈Ni≠j→imj=0˙
21 16 20 mpbird ⊢N∈Fin∧R∈Ring∧M∈S→S⊆D
22 simpr ⊢N∈Fin∧R∈Ring∧M∈S→M∈S
23 21 22 sseldd ⊢N∈Fin∧R∈Ring∧M∈S→M∈D
24 23 ex ⊢N∈Fin∧R∈Ring→M∈S→M∈D