Metamath Proof Explorer

Theorem dmatALTbasel

Description: An element of the base set of the algebra of N x N diagonal matrices over a ring R , i.e. an N x N diagonal matrix over the ring R . (Contributed by AV, 8-Dec-2019)

Ref Expression
Hypotheses dmatALTval.a ⊢ A = N Mat R
dmatALTval.b ⊢ B = Base A
dmatALTval.0 ⊢ 0 ˙ = 0 R
dmatALTval.d ⊢ D = N DMatALT R
Assertion dmatALTbasel ⊢ N ∈ Fin ∧ R ∈ V → M ∈ Base D ↔ M ∈ B ∧ ∀ i ∈ N ∀ j ∈ N i ≠ j → i M j = 0 ˙

Proof

Step Hyp Ref Expression
1 dmatALTval.a ⊢ A = N Mat R
2 dmatALTval.b ⊢ B = Base A
3 dmatALTval.0 ⊢ 0 ˙ = 0 R
4 dmatALTval.d ⊢ D = N DMatALT R
5 1 2 3 4 dmatALTbas ⊢ N ∈ Fin ∧ R ∈ V → Base D = m ∈ B | ∀ i ∈ N ∀ j ∈ N i ≠ j → i m j = 0 ˙
6 5 eleq2d ⊢ N ∈ Fin ∧ R ∈ V → M ∈ Base 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 ∈ Base D ↔ M ∈ B ∧ ∀ i ∈ N ∀ j ∈ N i ≠ j → i M j = 0 ˙