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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	marep01ma.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	marep01ma.r	⊢ 𝑅 ∈ CRing
	marep01ma.0	⊢ 0 = ( 0g ‘ 𝑅 )
	marep01ma.1	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	marep01ma	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		marep01ma.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		marep01ma.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		marep01ma.r	⊢ 𝑅 ∈ CRing
4		marep01ma.0	⊢ 0 = ( 0g ‘ 𝑅 )
5		marep01ma.1	⊢ 1 = ( 1r ‘ 𝑅 )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7	1 2	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
8	7	simpld	⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
9	3	a1i	⊢ ( 𝑀 ∈ 𝐵 → 𝑅 ∈ CRing )
10		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
11	6 5	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
12	3 10 11	mp2b	⊢ 1 ∈ ( Base ‘ 𝑅 )
13	6 4	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
14	3 10 13	mp2b	⊢ 0 ∈ ( Base ‘ 𝑅 )
15	12 14	ifcli	⊢ if ( 𝑙 = 𝐼 , 1 , 0 ) ∈ ( Base ‘ 𝑅 )
16	15	a1i	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → if ( 𝑙 = 𝐼 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
17		simp2	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
18		simp3	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑙 ∈ 𝑁 )
19		id	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ 𝐵 )
20	19 2	eleqtrdi	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( Base ‘ 𝐴 ) )
21	20	3ad2ant1	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝑀 ∈ ( Base ‘ 𝐴 ) )
22	1 6	matecl	⊢ ( ( 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ∧ 𝑀 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑘 𝑀 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
23	17 18 21 22	syl3anc	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑘 𝑀 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
24	16 23	ifcld	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ∈ ( Base ‘ 𝑅 ) )
25	1 6 2 8 9 24	matbas2d	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ if ( 𝑘 = 𝐻 , if ( 𝑙 = 𝐼 , 1 , 0 ) , ( 𝑘 𝑀 𝑙 ) ) ) ∈ 𝐵 )