Metamath Proof Explorer

Theorem dmatid

Description: The identity matrix is a diagonal matrix. (Contributed by AV, 19-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses dmatid.a ⊢ A = N Mat R
dmatid.b ⊢ B = Base A
dmatid.0 ⊢ 0 ˙ = 0 R
dmatid.d ⊢ D = N DMat R
Assertion dmatid ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ D

Proof

Step Hyp Ref Expression
1 dmatid.a ⊢ A = N Mat R
2 dmatid.b ⊢ B = Base A
3 dmatid.0 ⊢ 0 ˙ = 0 R
4 dmatid.d ⊢ D = N DMat R
5 1 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
6 eqid ⊢ 1 A = 1 A
7 2 6 ringidcl ⊢ A ∈ Ring → 1 A ∈ B
8 5 7 syl ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ B
9 eqid ⊢ 1 R = 1 R
10 simpl ⊢ N ∈ Fin ∧ R ∈ Ring → N ∈ Fin
11 10 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → N ∈ Fin
12 simpr ⊢ N ∈ Fin ∧ R ∈ Ring → R ∈ Ring
13 12 adantr ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → R ∈ Ring
14 simpl ⊢ i ∈ N ∧ j ∈ N → i ∈ N
15 14 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → i ∈ N
16 simpr ⊢ i ∈ N ∧ j ∈ N → j ∈ N
17 16 adantl ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → j ∈ N
18 1 9 3 11 13 15 17 6 mat1ov ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → i 1 A j = if i = j 1 R 0 ˙
19 ifnefalse ⊢ i ≠ j → if i = j 1 R 0 ˙ = 0 ˙
20 18 19 sylan9eq ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N ∧ i ≠ j → i 1 A j = 0 ˙
21 20 ex ⊢ N ∈ Fin ∧ R ∈ Ring ∧ i ∈ N ∧ j ∈ N → i ≠ j → i 1 A j = 0 ˙
22 21 ralrimivva ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ i ∈ N ∀ j ∈ N i ≠ j → i 1 A j = 0 ˙
23 1 2 3 4 dmatel ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ D ↔ 1 A ∈ B ∧ ∀ i ∈ N ∀ j ∈ N i ≠ j → i 1 A j = 0 ˙
24 8 22 23 mpbir2and ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A ∈ D