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 ( 𝑀 × 𝑀 ) ) )