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	$⊢ A = N Mat R$
	minmar1marrep.b	$⊢ B = {Base}_{A}$
	minmar1marrep.o	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	minmar1marrep	$⊢ (R \in Ring \land M \in B) \to (N minMatR1 R) (M) = M (N matRRep R) \underset{˙}{1}$

Step	Hyp	Ref	Expression
1		minmar1marrep.a	$⊢ A = N Mat R$
2		minmar1marrep.b	$⊢ B = {Base}_{A}$
3		minmar1marrep.o	$⊢ \underset{˙}{1} = 1_{R}$
4		eqid	$⊢ N minMatR1 R = N minMatR1 R$
5		eqid	$⊢ 0_{R} = 0_{R}$
6	1 2 4 3 5	minmar1val0	$⊢ M \in B \to (N minMatR1 R) (M) = (k \in N, l \in N ⟼ (i \in N, j \in N ⟼ if (i = k, if (j = l, \underset{˙}{1}, 0_{R}), i M j)))$
7	6	adantl	$⊢ (R \in Ring \land M \in B) \to (N minMatR1 R) (M) = (k \in N, l \in N ⟼ (i \in N, j \in N ⟼ if (i = k, if (j = l, \underset{˙}{1}, 0_{R}), i M j)))$
8		simpr	$⊢ (R \in Ring \land M \in B) \to M \in B$
9		eqid	$⊢ {Base}_{R} = {Base}_{R}$
10	9 3	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
11	10	adantr	$⊢ (R \in Ring \land M \in B) \to \underset{˙}{1} \in {Base}_{R}$
12		eqid	$⊢ N matRRep R = N matRRep R$
13	1 2 12 5	marrepval0	$⊢ (M \in B \land \underset{˙}{1} \in {Base}_{R}) \to M (N matRRep R) \underset{˙}{1} = (k \in N, l \in N ⟼ (i \in N, j \in N ⟼ if (i = k, if (j = l, \underset{˙}{1}, 0_{R}), i M j)))$
14	8 11 13	syl2anc	$⊢ (R \in Ring \land M \in B) \to M (N matRRep R) \underset{˙}{1} = (k \in N, l \in N ⟼ (i \in N, j \in N ⟼ if (i = k, if (j = l, \underset{˙}{1}, 0_{R}), i M j)))$
15	7 14	eqtr4d	$⊢ (R \in Ring \land M \in B) \to (N minMatR1 R) (M) = M (N matRRep R) \underset{˙}{1}$

Metamath Proof Explorer