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

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
mamumat1cl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mamumat1cl.o ⊢ 1 = ( 1r ‘ 𝑅 )
mamumat1cl.z ⊢ 0 = ( 0g ‘ 𝑅 )
mamumat1cl.i ⊢ 𝐼 = ( 𝑖 ∈ 𝑀 , 𝑗 ∈ 𝑀 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) )
mamumat1cl.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
Assertion mamumat1cl ( 𝜑 → 𝐼 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 mamumat1cl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mamumat1cl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 mamumat1cl.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 mamumat1cl.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 mamumat1cl.i ⊢ 𝐼 = ( 𝑖 ∈ 𝑀 , 𝑗 ∈ 𝑀 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) )
6 mamumat1cl.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
7 1 3 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
8 1 4 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐵 )
9 7 8 ifcld ⊢ ( 𝑅 ∈ Ring → if ( 𝑖 = 𝑗 , 1 , 0 ) ∈ 𝐵 )
10 2 9 syl ⊢ ( 𝜑 → if ( 𝑖 = 𝑗 , 1 , 0 ) ∈ 𝐵 )
11 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑗 ∈ 𝑀 ) ) → if ( 𝑖 = 𝑗 , 1 , 0 ) ∈ 𝐵 )
12 11 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑀 ∀ 𝑗 ∈ 𝑀 if ( 𝑖 = 𝑗 , 1 , 0 ) ∈ 𝐵 )
13 5 fmpo ⊢ ( ∀ 𝑖 ∈ 𝑀 ∀ 𝑗 ∈ 𝑀 if ( 𝑖 = 𝑗 , 1 , 0 ) ∈ 𝐵 ↔ 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
14 12 13 sylib ⊢ ( 𝜑 → 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 )
15 1 fvexi ⊢ 𝐵 ∈ V
16 xpfi ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑀 ∈ Fin ) → ( 𝑀 × 𝑀 ) ∈ Fin )
17 6 6 16 syl2anc ⊢ ( 𝜑 → ( 𝑀 × 𝑀 ) ∈ Fin )
18 elmapg ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑀 × 𝑀 ) ∈ Fin ) → ( 𝐼 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑀 ) ) ↔ 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 ) )
19 15 17 18 sylancr ⊢ ( 𝜑 → ( 𝐼 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑀 ) ) ↔ 𝐼 : ( 𝑀 × 𝑀 ) ⟶ 𝐵 ) )
20 14 19 mpbird ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑀 ) ) )