Theorem minmar1marrep

Description: The minor matrix is a special case of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019) (Revised by AV, 4-Jul-2022)

	Ref	Expression
Hypotheses	minmar1marrep.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	minmar1marrep.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	minmar1marrep.o	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	minmar1marrep	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) 1 ) )

Proof

Step	Hyp	Ref	Expression
1		minmar1marrep.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		minmar1marrep.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		minmar1marrep.o	⊢ 1 = ( 1r ‘ 𝑅 )
4		eqid	⊢ ( 𝑁 minMatR1 𝑅 ) = ( 𝑁 minMatR1 𝑅 )
5		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6	1 2 4 3 5	minmar1val0	⊢ ( 𝑀 ∈ 𝐵 → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
7	6	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
8		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
9		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10	9 3	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
11	10	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 1 ∈ ( Base ‘ 𝑅 ) )
12		eqid	⊢ ( 𝑁 matRRep 𝑅 ) = ( 𝑁 matRRep 𝑅 )
13	1 2 12 5	marrepval0	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑀 ( 𝑁 matRRep 𝑅 ) 1 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
14	8 11 13	syl2anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 𝑀 ( 𝑁 matRRep 𝑅 ) 1 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , ( 0g ‘ 𝑅 ) ) , ( 𝑖 𝑀 𝑗 ) ) ) ) )
15	7 14	eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝑁 minMatR1 𝑅 ) ‘ 𝑀 ) = ( 𝑀 ( 𝑁 matRRep 𝑅 ) 1 ) )