ma1repvcl

Description: Closure of the column replacement function for identity matrices. (Contributed by AV, 15-Feb-2019) (Revised by AV, 26-Feb-2019)

	Ref	Expression
Hypotheses	marepvcl.a	$⊢ A = N Mat R$
	marepvcl.b	$⊢ B = {Base}_{A}$
	marepvcl.v	$⊢ V = {Base}_{R}^{N}$
	ma1repvcl.1	$⊢ \underset{˙}{1} = 1_{A}$
Assertion	ma1repvcl	$⊢ ((R \in Ring \land N \in Fin) \land (C \in V \land K \in N)) \to (\underset{˙}{1} (N matRepV R) C) (K) \in B$

Step	Hyp	Ref	Expression
1		marepvcl.a	$⊢ A = N Mat R$
2		marepvcl.b	$⊢ B = {Base}_{A}$
3		marepvcl.v	$⊢ V = {Base}_{R}^{N}$
4		ma1repvcl.1	$⊢ \underset{˙}{1} = 1_{A}$
5		simpll	$⊢ ((R \in Ring \land N \in Fin) \land (C \in V \land K \in N)) \to R \in Ring$
6	1	fveq2i	$⊢ 1_{A} = 1_{(N Mat R)}$
7	4 6	eqtri	$⊢ \underset{˙}{1} = 1_{(N Mat R)}$
8	1 2 7	mat1bas	$⊢ (R \in Ring \land N \in Fin) \to \underset{˙}{1} \in B$
9	8	anim1i	$⊢ ((R \in Ring \land N \in Fin) \land (C \in V \land K \in N)) \to (\underset{˙}{1} \in B \land (C \in V \land K \in N))$
10		3anass	$⊢ (\underset{˙}{1} \in B \land C \in V \land K \in N) \leftrightarrow (\underset{˙}{1} \in B \land (C \in V \land K \in N))$
11	9 10	sylibr	$⊢ ((R \in Ring \land N \in Fin) \land (C \in V \land K \in N)) \to (\underset{˙}{1} \in B \land C \in V \land K \in N)$
12	1 2 3	marepvcl	$⊢ (R \in Ring \land (\underset{˙}{1} \in B \land C \in V \land K \in N)) \to (\underset{˙}{1} (N matRepV R) C) (K) \in B$
13	5 11 12	syl2anc	$⊢ ((R \in Ring \land N \in Fin) \land (C \in V \land K \in N)) \to (\underset{˙}{1} (N matRepV R) C) (K) \in B$

Metamath Proof Explorer