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 = N Mat R
scmatid.b ⊢ B = Base A
scmatid.e ⊢ E = Base R
scmatid.0 ⊢ 0 ˙ = 0 R
scmatid.s ⊢ S = N ScMat R
scmatdmat.d ⊢ D = N DMat R
Assertion scmatdmat ⊢ N ∈ Fin ∧ R ∈ Ring → M ∈ S → M ∈ D

Proof

Step Hyp Ref Expression
1 scmatid.a ⊢ A = N Mat R
2 scmatid.b ⊢ B = Base A
3 scmatid.e ⊢ E = Base R
4 scmatid.0 ⊢ 0 ˙ = 0 R
5 scmatid.s ⊢ S = N ScMat R
6 scmatdmat.d ⊢ D = N DMat R
7 id ⊢ i m j = if i = j c 0 ˙ → i m j = if i = j c 0 ˙
8 ifnefalse ⊢ i ≠ j → if i = j c 0 ˙ = 0 ˙
9 7 8 sylan9eq ⊢ i m j = if i = j c 0 ˙ ∧ i ≠ j → i m j = 0 ˙
10 9 ex ⊢ i m j = if i = j c 0 ˙ → i ≠ j → i m j = 0 ˙
11 10 a1i ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ E ∧ i ∈ N ∧ j ∈ N → i m j = if i = j c 0 ˙ → i ≠ j → i m j = 0 ˙
12 11 ralimdva ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ E ∧ i ∈ N → ∀ j ∈ N i m j = if i = j c 0 ˙ → ∀ j ∈ N i ≠ j → i m j = 0 ˙
13 12 ralimdva ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B ∧ c ∈ E → ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ → ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙
14 13 rexlimdva ⊢ N ∈ Fin ∧ R ∈ Ring ∧ m ∈ B → ∃ c ∈ E ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ → ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙
15 14 ss2rabdv ⊢ N ∈ Fin ∧ R ∈ Ring → m ∈ B | ∃ c ∈ E ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ ⊆ m ∈ B | ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙
16 15 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → m ∈ B | ∃ c ∈ E ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ ⊆ m ∈ B | ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙
17 1 2 5 3 4 scmatmats ⊢ N ∈ Fin ∧ R ∈ Ring → S = m ∈ B | ∃ c ∈ E ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙
18 1 2 4 6 dmatval ⊢ N ∈ Fin ∧ R ∈ Ring → D = m ∈ B | ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙
19 17 18 sseq12d ⊢ N ∈ Fin ∧ R ∈ Ring → S ⊆ D ↔ m ∈ B | ∃ c ∈ E ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ ⊆ m ∈ B | ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙
20 19 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ S → S ⊆ D ↔ m ∈ B | ∃ c ∈ E ∀ i ∈ N ∀ j ∈ N i m j = if i = j c 0 ˙ ⊆ m ∈ B | ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 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