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