mulmarep1el

Description: Element by element multiplication of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 16-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}$
	mulmarep1el.0	$⊢ \underset{˙}{0} = 0_{R}$
	mulmarep1el.e	$⊢ E = (\underset{˙}{1} (N matRepV R) C) (K)$
Assertion	mulmarep1el	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to (I X L) \cdot_{R} (L E J) = if (J = K, (I X L) \cdot_{R} C (L), if (J = L, I X L, \underset{˙}{0}))$

Proof

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		mulmarep1el.0	$⊢ \underset{˙}{0} = 0_{R}$
6		mulmarep1el.e	$⊢ E = (\underset{˙}{1} (N matRepV R) C) (K)$
7		simp3	$⊢ (I \in N \land J \in N \land L \in N) \to L \in N$
8		simp2	$⊢ (I \in N \land J \in N \land L \in N) \to J \in N$
9	7 8	jca	$⊢ (I \in N \land J \in N \land L \in N) \to (L \in N \land J \in N)$
10	1 2 3 4 5 6	ma1repveval	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (L \in N \land J \in N)) \to L E J = if (J = K, C (L), if (J = L, 1_{R}, \underset{˙}{0}))$
11	9 10	syl3an3	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to L E J = if (J = K, C (L), if (J = L, 1_{R}, \underset{˙}{0}))$
12	11	oveq2d	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to (I X L) \cdot_{R} (L E J) = (I X L) \cdot_{R} if (J = K, C (L), if (J = L, 1_{R}, \underset{˙}{0}))$
13		ovif2	$⊢ (I X L) \cdot_{R} if (J = K, C (L), if (J = L, 1_{R}, \underset{˙}{0})) = if (J = K, (I X L) \cdot_{R} C (L), (I X L) \cdot_{R} if (J = L, 1_{R}, \underset{˙}{0}))$
14	13	a1i	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to (I X L) \cdot_{R} if (J = K, C (L), if (J = L, 1_{R}, \underset{˙}{0})) = if (J = K, (I X L) \cdot_{R} C (L), (I X L) \cdot_{R} if (J = L, 1_{R}, \underset{˙}{0}))$
15		ovif2	$⊢ (I X L) \cdot_{R} if (J = L, 1_{R}, \underset{˙}{0}) = if (J = L, (I X L) \cdot_{R} 1_{R}, (I X L) \cdot_{R} \underset{˙}{0})$
16		simp1	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to R \in Ring$
17		simp1	$⊢ (I \in N \land J \in N \land L \in N) \to I \in N$
18	17	3ad2ant3	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to I \in N$
19	7	3ad2ant3	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to L \in N$
20	2	eleq2i	$⊢ X \in B \leftrightarrow X \in {Base}_{A}$
21	20	biimpi	$⊢ X \in B \to X \in {Base}_{A}$
22	21	3ad2ant1	$⊢ (X \in B \land C \in V \land K \in N) \to X \in {Base}_{A}$
23	22	3ad2ant2	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to X \in {Base}_{A}$
24		eqid	$⊢ {Base}_{R} = {Base}_{R}$
25	1 24	matecl	$⊢ (I \in N \land L \in N \land X \in {Base}_{A}) \to I X L \in {Base}_{R}$
26	18 19 23 25	syl3anc	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to I X L \in {Base}_{R}$
27		eqid	$⊢ \cdot_{R} = \cdot_{R}$
28		eqid	$⊢ 1_{R} = 1_{R}$
29	24 27 28	ringridm	$⊢ (R \in Ring \land I X L \in {Base}_{R}) \to (I X L) \cdot_{R} 1_{R} = I X L$
30	16 26 29	syl2anc	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to (I X L) \cdot_{R} 1_{R} = I X L$
31	24 27 5	ringrz	$⊢ (R \in Ring \land I X L \in {Base}_{R}) \to (I X L) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
32	16 26 31	syl2anc	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to (I X L) \cdot_{R} \underset{˙}{0} = \underset{˙}{0}$
33	30 32	ifeq12d	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to if (J = L, (I X L) \cdot_{R} 1_{R}, (I X L) \cdot_{R} \underset{˙}{0}) = if (J = L, I X L, \underset{˙}{0})$
34	15 33	syl5eq	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to (I X L) \cdot_{R} if (J = L, 1_{R}, \underset{˙}{0}) = if (J = L, I X L, \underset{˙}{0})$
35	34	ifeq2d	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to if (J = K, (I X L) \cdot_{R} C (L), (I X L) \cdot_{R} if (J = L, 1_{R}, \underset{˙}{0})) = if (J = K, (I X L) \cdot_{R} C (L), if (J = L, I X L, \underset{˙}{0}))$
36	12 14 35	3eqtrd	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land L \in N)) \to (I X L) \cdot_{R} (L E J) = if (J = K, (I X L) \cdot_{R} C (L), if (J = L, I X L, \underset{˙}{0}))$

Metamath Proof Explorer

Theorem mulmarep1el

Proof