marrepeval

Description: An entry of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019)

	Ref	Expression
Hypotheses	marrepfval.a	$⊢ A = N Mat R$
	marrepfval.b	$⊢ B = {Base}_{A}$
	marrepfval.q	$⊢ Q = N matRRep R$
	marrepfval.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	marrepeval	$⊢ ((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 (K (M Q S) L) J = if (I = K, if (J = L, S, \underset{˙}{0}), I M J)$

Proof

Step	Hyp	Ref	Expression
1		marrepfval.a	$⊢ A = N Mat R$
2		marrepfval.b	$⊢ B = {Base}_{A}$
3		marrepfval.q	$⊢ Q = N matRRep R$
4		marrepfval.z	$⊢ \underset{˙}{0} = 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 Q S) L = (i \in N, j \in N ⟼ if (i = K, if (j = L, S, \underset{˙}{0}), i M j))$
6	5	3adant3	$⊢ ((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 K (M Q S) L = (i \in N, j \in N ⟼ if (i = K, if (j = L, S, \underset{˙}{0}), i M j))$
7		simp3l	$⊢ ((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$
8		simpl3r	$⊢ (((M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N) \land (I \in N \land J \in N)) \land i = I) \to J \in N$
9	4	fvexi	$⊢ \underset{˙}{0} \in V$
10		ifexg	$⊢ (S \in {Base}_{R} \land \underset{˙}{0} \in V) \to if (j = L, S, \underset{˙}{0}) \in V$
11	9 10	mpan2	$⊢ S \in {Base}_{R} \to if (j = L, S, \underset{˙}{0}) \in V$
12		ovexd	$⊢ S \in {Base}_{R} \to i M j \in V$
13	11 12	ifcld	$⊢ S \in {Base}_{R} \to if (i = K, if (j = L, S, \underset{˙}{0}), i M j) \in V$
14	13	adantl	$⊢ (M \in B \land S \in {Base}_{R}) \to if (i = K, if (j = L, S, \underset{˙}{0}), i M j) \in V$
15	14	3ad2ant1	$⊢ ((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, \underset{˙}{0}), i M j) \in V$
16	15	adantr	$⊢ (((M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N) \land (I \in N \land J \in N)) \land (i = I \land j = J)) \to if (i = K, if (j = L, S, \underset{˙}{0}), i M j) \in V$
17		eqeq1	$⊢ i = I \to (i = K \leftrightarrow I = K)$
18	17	adantr	$⊢ (i = I \land j = J) \to (i = K \leftrightarrow I = K)$
19		eqeq1	$⊢ j = J \to (j = L \leftrightarrow J = L)$
20	19	ifbid	$⊢ j = J \to if (j = L, S, \underset{˙}{0}) = if (J = L, S, \underset{˙}{0})$
21	20	adantl	$⊢ (i = I \land j = J) \to if (j = L, S, \underset{˙}{0}) = if (J = L, S, \underset{˙}{0})$
22		oveq12	$⊢ (i = I \land j = J) \to i M j = I M J$
23	18 21 22	ifbieq12d	$⊢ (i = I \land j = J) \to if (i = K, if (j = L, S, \underset{˙}{0}), i M j) = if (I = K, if (J = L, S, \underset{˙}{0}), I M J)$
24	23	adantl	$⊢ (((M \in B \land S \in {Base}_{R}) \land (K \in N \land L \in N) \land (I \in N \land J \in N)) \land (i = I \land j = J)) \to if (i = K, if (j = L, S, \underset{˙}{0}), i M j) = if (I = K, if (J = L, S, \underset{˙}{0}), I M J)$
25	7 8 16 24	ovmpodv2	$⊢ ((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 (K (M Q S) L = (i \in N, j \in N ⟼ if (i = K, if (j = L, S, \underset{˙}{0}), i M j)) \to I (K (M Q S) L) J = if (I = K, if (J = L, S, \underset{˙}{0}), I M J))$
26	6 25	mpd	$⊢ ((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 (K (M Q S) L) J = if (I = K, if (J = L, S, \underset{˙}{0}), I M J)$

Metamath Proof Explorer

Theorem marrepeval

Proof