minmar1cl

Description: Closure of the row replacement function for square matrices: The matrix for a minor is a matrix. (Contributed by AV, 13-Feb-2019)

	Ref	Expression
Hypotheses	minmar1cl.a	$⊢ A = N Mat R$
	minmar1cl.b	$⊢ B = {Base}_{A}$
Assertion	minmar1cl	$⊢ ((R \in Ring \land M \in B) \land (K \in N \land L \in N)) \to K (N minMatR1 R) (M) L \in B$

Step	Hyp	Ref	Expression
1		minmar1cl.a	$⊢ A = N Mat R$
2		minmar1cl.b	$⊢ B = {Base}_{A}$
3		eqid	$⊢ 1_{R} = 1_{R}$
4	1 2 3	minmar1marrep	$⊢ (R \in Ring \land M \in B) \to (N minMatR1 R) (M) = M (N matRRep R) 1_{R}$
5	4	adantr	$⊢ ((R \in Ring \land M \in B) \land (K \in N \land L \in N)) \to (N minMatR1 R) (M) = M (N matRRep R) 1_{R}$
6	5	oveqd	$⊢ ((R \in Ring \land M \in B) \land (K \in N \land L \in N)) \to K (N minMatR1 R) (M) L = K (M (N matRRep R) 1_{R}) L$
7		simpl	$⊢ (R \in Ring \land M \in B) \to R \in Ring$
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 1_{R} \in {Base}_{R}$
11	10	adantr	$⊢ (R \in Ring \land M \in B) \to 1_{R} \in {Base}_{R}$
12	7 8 11	3jca	$⊢ (R \in Ring \land M \in B) \to (R \in Ring \land M \in B \land 1_{R} \in {Base}_{R})$
13	1 2	marrepcl	$⊢ ((R \in Ring \land M \in B \land 1_{R} \in {Base}_{R}) \land (K \in N \land L \in N)) \to K (M (N matRRep R) 1_{R}) L \in B$
14	12 13	sylan	$⊢ ((R \in Ring \land M \in B) \land (K \in N \land L \in N)) \to K (M (N matRRep R) 1_{R}) L \in B$
15	6 14	eqeltrd	$⊢ ((R \in Ring \land M \in B) \land (K \in N \land L \in N)) \to K (N minMatR1 R) (M) L \in B$

Metamath Proof Explorer