Metamath Proof Explorer

Theorem mat1ov

Description: Entries of an identity matrix, deduction form. (Contributed by Stefan O'Rear, 10-Jul-2018)

Ref Expression
Hypotheses mat1.a ⊢ A = N Mat R
mat1.o ⊢ 1 ˙ = 1 R
mat1.z ⊢ 0 ˙ = 0 R
mat1ov.n ⊢ φ → N ∈ Fin
mat1ov.r ⊢ φ → R ∈ Ring
mat1ov.i ⊢ φ → I ∈ N
mat1ov.j ⊢ φ → J ∈ N
mat1ov.u ⊢ U = 1 A
Assertion mat1ov ⊢ φ → I U J = if I = J 1 ˙ 0 ˙

Proof

Step Hyp Ref Expression
1 mat1.a ⊢ A = N Mat R
2 mat1.o ⊢ 1 ˙ = 1 R
3 mat1.z ⊢ 0 ˙ = 0 R
4 mat1ov.n ⊢ φ → N ∈ Fin
5 mat1ov.r ⊢ φ → R ∈ Ring
6 mat1ov.i ⊢ φ → I ∈ N
7 mat1ov.j ⊢ φ → J ∈ N
8 mat1ov.u ⊢ U = 1 A
9 1 2 3 mat1 ⊢ N ∈ Fin ∧ R ∈ Ring → 1 A = i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙
10 4 5 9 syl2anc ⊢ φ → 1 A = i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙
11 8 10 eqtrid ⊢ φ → U = i ∈ N , j ∈ N ⟼ if i = j 1 ˙ 0 ˙
12 eqeq12 ⊢ i = I ∧ j = J → i = j ↔ I = J
13 12 ifbid ⊢ i = I ∧ j = J → if i = j 1 ˙ 0 ˙ = if I = J 1 ˙ 0 ˙
14 13 adantl ⊢ φ ∧ i = I ∧ j = J → if i = j 1 ˙ 0 ˙ = if I = J 1 ˙ 0 ˙
15 2 fvexi ⊢ 1 ˙ ∈ V
16 3 fvexi ⊢ 0 ˙ ∈ V
17 15 16 ifex ⊢ if I = J 1 ˙ 0 ˙ ∈ V
18 17 a1i ⊢ φ → if I = J 1 ˙ 0 ˙ ∈ V
19 11 14 6 7 18 ovmpod ⊢ φ → I U J = if I = J 1 ˙ 0 ˙