Theorem marep01ma

Description: Replacing a row of a square matrix by a row with 0's and a 1 results in a square matrix of the same dimension. (Contributed by AV, 30-Dec-2018)

	Ref	Expression
Hypotheses	marep01ma.a	|- A = ( N Mat R )
	marep01ma.b	|- B = ( Base ` A )
	marep01ma.r	|- R e. CRing
	marep01ma.0	|- .0. = ( 0g ` R )
	marep01ma.1	|- .1. = ( 1r ` R )
Assertion	marep01ma	|- ( M e. B -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) e. B )

Proof

Step	Hyp	Ref	Expression
1		marep01ma.a	|- A = ( N Mat R )
2		marep01ma.b	|- B = ( Base ` A )
3		marep01ma.r	|- R e. CRing
4		marep01ma.0	|- .0. = ( 0g ` R )
5		marep01ma.1	|- .1. = ( 1r ` R )
6		eqid	|- ( Base ` R ) = ( Base ` R )
7	1 2	matrcl	|- ( M e. B -> ( N e. Fin /\ R e. _V ) )
8	7	simpld	|- ( M e. B -> N e. Fin )
9	3	a1i	|- ( M e. B -> R e. CRing )
10		crngring	|- ( R e. CRing -> R e. Ring )
11	6 5	ringidcl	|- ( R e. Ring -> .1. e. ( Base ` R ) )
12	3 10 11	mp2b	|- .1. e. ( Base ` R )
13	6 4	ring0cl	|- ( R e. Ring -> .0. e. ( Base ` R ) )
14	3 10 13	mp2b	|- .0. e. ( Base ` R )
15	12 14	ifcli	|- if ( l = I , .1. , .0. ) e. ( Base ` R )
16	15	a1i	|- ( ( M e. B /\ k e. N /\ l e. N ) -> if ( l = I , .1. , .0. ) e. ( Base ` R ) )
17		simp2	|- ( ( M e. B /\ k e. N /\ l e. N ) -> k e. N )
18		simp3	|- ( ( M e. B /\ k e. N /\ l e. N ) -> l e. N )
19		id	|- ( M e. B -> M e. B )
20	19 2	eleqtrdi	|- ( M e. B -> M e. ( Base ` A ) )
21	20	3ad2ant1	|- ( ( M e. B /\ k e. N /\ l e. N ) -> M e. ( Base ` A ) )
22	1 6	matecl	|- ( ( k e. N /\ l e. N /\ M e. ( Base ` A ) ) -> ( k M l ) e. ( Base ` R ) )
23	17 18 21 22	syl3anc	|- ( ( M e. B /\ k e. N /\ l e. N ) -> ( k M l ) e. ( Base ` R ) )
24	16 23	ifcld	|- ( ( M e. B /\ k e. N /\ l e. N ) -> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) e. ( Base ` R ) )
25	1 6 2 8 9 24	matbas2d	|- ( M e. B -> ( k e. N , l e. N |-> if ( k = H , if ( l = I , .1. , .0. ) , ( k M l ) ) ) e. B )