This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mat1comp

Description: The components of the identity matrix (as operation in maps-to notation). (Contributed by AV, 22-Jul-2019)

Ref Expression
Hypotheses mamumat1cl.b ⊢ B = Base R
mamumat1cl.r ⊢ φ → R ∈ Ring
mamumat1cl.o ⊢ 1 ˙ = 1 R
mamumat1cl.z ⊢ 0 ˙ = 0 R
mamumat1cl.i ⊢ I = i ∈ M , j ∈ M ⟼ if i = j 1 ˙ 0 ˙
mamumat1cl.m ⊢ φ → M ∈ Fin
Assertion mat1comp ⊢ A ∈ M ∧ J ∈ M → A I J = if A = J 1 ˙ 0 ˙

Proof

Step Hyp Ref Expression
1 mamumat1cl.b ⊢ B = Base R
2 mamumat1cl.r ⊢ φ → R ∈ Ring
3 mamumat1cl.o ⊢ 1 ˙ = 1 R
4 mamumat1cl.z ⊢ 0 ˙ = 0 R
5 mamumat1cl.i ⊢ I = i ∈ M , j ∈ M ⟼ if i = j 1 ˙ 0 ˙
6 mamumat1cl.m ⊢ φ → M ∈ Fin
7 eqeq1 ⊢ i = A → i = j ↔ A = j
8 7 ifbid ⊢ i = A → if i = j 1 ˙ 0 ˙ = if A = j 1 ˙ 0 ˙
9 eqeq2 ⊢ j = J → A = j ↔ A = J
10 9 ifbid ⊢ j = J → if A = j 1 ˙ 0 ˙ = if A = J 1 ˙ 0 ˙
11 3 fvexi ⊢ 1 ˙ ∈ V
12 4 fvexi ⊢ 0 ˙ ∈ V
13 11 12 ifex ⊢ if A = J 1 ˙ 0 ˙ ∈ V
14 8 10 5 13 ovmpo ⊢ A ∈ M ∧ J ∈ M → A I J = if A = J 1 ˙ 0 ˙