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	|- B = ( Base ` R )
	mamumat1cl.r	|- ( ph -> R e. Ring )
	mamumat1cl.o	|- .1. = ( 1r ` R )
	mamumat1cl.z	|- .0. = ( 0g ` R )
	mamumat1cl.i	|- I = ( i e. M , j e. M |-> if ( i = j , .1. , .0. ) )
	mamumat1cl.m	|- ( ph -> M e. Fin )
Assertion	mat1comp	|- ( ( A e. M /\ J e. M ) -> ( A I J ) = if ( A = J , .1. , .0. ) )

Proof

Step	Hyp	Ref	Expression
1		mamumat1cl.b	|- B = ( Base ` R )
2		mamumat1cl.r	|- ( ph -> R e. Ring )
3		mamumat1cl.o	|- .1. = ( 1r ` R )
4		mamumat1cl.z	|- .0. = ( 0g ` R )
5		mamumat1cl.i	|- I = ( i e. M , j e. M |-> if ( i = j , .1. , .0. ) )
6		mamumat1cl.m	|- ( ph -> M e. Fin )
7		eqeq1	|- ( i = A -> ( i = j <-> A = j ) )
8	7	ifbid	|- ( i = A -> if ( i = j , .1. , .0. ) = if ( A = j , .1. , .0. ) )
9		eqeq2	|- ( j = J -> ( A = j <-> A = J ) )
10	9	ifbid	|- ( j = J -> if ( A = j , .1. , .0. ) = if ( A = J , .1. , .0. ) )
11	3	fvexi	|- .1. e. _V
12	4	fvexi	|- .0. e. _V
13	11 12	ifex	|- if ( A = J , .1. , .0. ) e. _V
14	8 10 5 13	ovmpo	|- ( ( A e. M /\ J e. M ) -> ( A I J ) = if ( A = J , .1. , .0. ) )