Theorem mat1comp

Description: The components of the identity matrix (as operation in maps-to notation). (Contributed by AV, 22-Jul-2019)

	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	mat1comp	⊢ ( ( 𝐴 ∈ 𝑀 ∧ 𝐽 ∈ 𝑀 ) → ( 𝐴 𝐼 𝐽 ) = if ( 𝐴 = 𝐽 , 1 , 0 ) )

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		eqeq1	⊢ ( 𝑖 = 𝐴 → ( 𝑖 = 𝑗 ↔ 𝐴 = 𝑗 ) )
8	7	ifbid	⊢ ( 𝑖 = 𝐴 → if ( 𝑖 = 𝑗 , 1 , 0 ) = if ( 𝐴 = 𝑗 , 1 , 0 ) )
9		eqeq2	⊢ ( 𝑗 = 𝐽 → ( 𝐴 = 𝑗 ↔ 𝐴 = 𝐽 ) )
10	9	ifbid	⊢ ( 𝑗 = 𝐽 → if ( 𝐴 = 𝑗 , 1 , 0 ) = if ( 𝐴 = 𝐽 , 1 , 0 ) )
11	3	fvexi	⊢ 1 ∈ V
12	4	fvexi	⊢ 0 ∈ V
13	11 12	ifex	⊢ if ( 𝐴 = 𝐽 , 1 , 0 ) ∈ V
14	8 10 5 13	ovmpo	⊢ ( ( 𝐴 ∈ 𝑀 ∧ 𝐽 ∈ 𝑀 ) → ( 𝐴 𝐼 𝐽 ) = if ( 𝐴 = 𝐽 , 1 , 0 ) )