marrepcl

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

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

Proof

Step	Hyp	Ref	Expression
1		marrepcl.a	$⊢ A = N Mat R$
2		marrepcl.b	$⊢ B = {Base}_{A}$
3		eqid	$⊢ N matRRep R = N matRRep R$
4		eqid	$⊢ 0_{R} = 0_{R}$
5	1 2 3 4	marrepval	$⊢ ((M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \to K (M (N matRRep R) S) L = (i \in N, j \in N ⟼ if (i = K, if (j = L, S, 0_{R}), i M j))$
6	5	3adantl1	$⊢ ((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \to K (M (N matRRep R) S) L = (i \in N, j \in N ⟼ if (i = K, if (j = L, S, 0_{R}), i M j))$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
9	8	simpld	$⊢ M \in B \to N \in Fin$
10	9	3ad2ant2	$⊢ (R \in Ring \land M \in B \land S \in {Base}_{R}) \to N \in Fin$
11	10	adantr	$⊢ ((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \to N \in Fin$
12		simpl1	$⊢ ((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \to R \in Ring$
13		simp3	$⊢ (R \in Ring \land M \in B \land S \in {Base}_{R}) \to S \in {Base}_{R}$
14	7 4	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
15	14	3ad2ant1	$⊢ (R \in Ring \land M \in B \land S \in {Base}_{R}) \to 0_{R} \in {Base}_{R}$
16	13 15	ifcld	$⊢ (R \in Ring \land M \in B \land S \in {Base}_{R}) \to if (j = L, S, 0_{R}) \in {Base}_{R}$
17	16	adantr	$⊢ ((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \to if (j = L, S, 0_{R}) \in {Base}_{R}$
18	17	3ad2ant1	$⊢ (((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \land i \in N \land j \in N) \to if (j = L, S, 0_{R}) \in {Base}_{R}$
19		simp2	$⊢ (((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \land i \in N \land j \in N) \to i \in N$
20		simp3	$⊢ (((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \land i \in N \land j \in N) \to j \in N$
21	2	eleq2i	$⊢ M \in B \leftrightarrow M \in {Base}_{A}$
22	21	biimpi	$⊢ M \in B \to M \in {Base}_{A}$
23	22	3ad2ant2	$⊢ (R \in Ring \land M \in B \land S \in {Base}_{R}) \to M \in {Base}_{A}$
24	23	adantr	$⊢ ((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \to M \in {Base}_{A}$
25	24	3ad2ant1	$⊢ (((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \land i \in N \land j \in N) \to M \in {Base}_{A}$
26	1 7	matecl	$⊢ (i \in N \land j \in N \land M \in {Base}_{A}) \to i M j \in {Base}_{R}$
27	19 20 25 26	syl3anc	$⊢ (((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \land i \in N \land j \in N) \to i M j \in {Base}_{R}$
28	18 27	ifcld	$⊢ (((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \land i \in N \land j \in N) \to if (i = K, if (j = L, S, 0_{R}), i M j) \in {Base}_{R}$
29	1 7 2 11 12 28	matbas2d	$⊢ ((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \to (i \in N, j \in N ⟼ if (i = K, if (j = L, S, 0_{R}), i M j)) \in B$
30	6 29	eqeltrd	$⊢ ((R \in Ring \land M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N)) \to K (M (N matRRep R) S) L \in B$

Metamath Proof Explorer

Theorem marrepcl

Proof