Metamath Proof Explorer

Theorem mamumat1cl

Description: The identity matrix (as operation in maps-to notation) is a matrix. (Contributed by Stefan O'Rear, 2-Sep-2015)

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 mamumat1cl ⊢ φ → I ∈ B M × M

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 1 3 ringidcl ⊢ R ∈ Ring → 1 ˙ ∈ B
8 1 4 ring0cl ⊢ R ∈ Ring → 0 ˙ ∈ B
9 7 8 ifcld ⊢ R ∈ Ring → if i = j 1 ˙ 0 ˙ ∈ B
10 2 9 syl ⊢ φ → if i = j 1 ˙ 0 ˙ ∈ B
11 10 adantr ⊢ φ ∧ i ∈ M ∧ j ∈ M → if i = j 1 ˙ 0 ˙ ∈ B
12 11 ralrimivva ⊢ φ → ∀ i ∈ M ∀ j ∈ M if i = j 1 ˙ 0 ˙ ∈ B
13 5 fmpo ⊢ ∀ i ∈ M ∀ j ∈ M if i = j 1 ˙ 0 ˙ ∈ B ↔ I : M × M ⟶ B
14 12 13 sylib ⊢ φ → I : M × M ⟶ B
15 1 fvexi ⊢ B ∈ V
16 xpfi ⊢ M ∈ Fin ∧ M ∈ Fin → M × M ∈ Fin
17 6 6 16 syl2anc ⊢ φ → M × M ∈ Fin
18 elmapg ⊢ B ∈ V ∧ M × M ∈ Fin → I ∈ B M × M ↔ I : M × M ⟶ B
19 15 17 18 sylancr ⊢ φ → I ∈ B M × M ↔ I : M × M ⟶ B
20 14 19 mpbird ⊢ φ → I ∈ B M × M