Metamath Proof Explorer

Theorem dmatel

Description: A N x N diagonal matrix over (a ring) R . (Contributed by AV, 18-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 dmatel ⊢ N ∈ Fin ∧ R ∈ V → M ∈ 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 1 2 3 4 dmatval ⊢ N ∈ Fin ∧ R ∈ V → D = m ∈ B | ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙
6 5 eleq2d ⊢ N ∈ Fin ∧ R ∈ V → M ∈ D ↔ M ∈ m ∈ B | ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙
7 oveq ⊢ m = M → i m j = i M j
8 7 eqeq1d ⊢ m = M → i m j = 0 ˙ ↔ i M j = 0 ˙
9 8 imbi2d ⊢ m = M → i ≠ j → i m j = 0 ˙ ↔ i ≠ j → i M j = 0 ˙
10 9 2ralbidv ⊢ m = M → ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙ ↔ ∀ i ∈ N ∀ j ∈ N i ≠ j → i M j = 0 ˙
11 10 elrab ⊢ M ∈ m ∈ B | ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙ ↔ M ∈ B ∧ ∀ i ∈ N ∀ j ∈ N i ≠ j → i M j = 0 ˙
12 6 11 bitrdi ⊢ N ∈ Fin ∧ R ∈ V → M ∈ D ↔ M ∈ B ∧ ∀ i ∈ N ∀ j ∈ N i ≠ j → i M j = 0 ˙