mulmarep1gsum2

Description: The sum of element by element multiplications of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 18-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)$
	mulmarep1gsum2.x	$⊢ \underset{˙}{\times} = R maVecMul ⟨N, N⟩$
Assertion	mulmarep1gsum2	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = if (J = K, Z (I), I X J)$

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		mulmarep1gsum2.x	$⊢ \underset{˙}{\times} = R maVecMul ⟨N, N⟩$
8		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 X \underset{˙}{\times} C = Z)) \to R \in Ring$
9	8	adantr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land l \in N) \to R \in Ring$
10		simpl2	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land l \in N) \to (X \in B \land C \in V \land K \in N)$
11		simp1	$⊢ (I \in N \land J \in N \land X \underset{˙}{\times} C = Z) \to I \in N$
12	11	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 X \underset{˙}{\times} C = Z)) \to I \in N$
13	12	adantr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land l \in N) \to I \in N$
14		simpl32	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land l \in N) \to J \in N$
15		simpr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land l \in N) \to l \in N$
16	13 14 15	3jca	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land l \in N) \to (I \in N \land J \in N \land l \in N)$
17	9 10 16	3jca	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land l \in N) \to (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))$
18	17	adantll	$⊢ ((J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \land l \in N) \to (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))$
19	1 2 3 4 5 6	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}))$
20	18 19	syl	$⊢ ((J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \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}))$
21		iftrue	$⊢ J = K \to if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0})) = (I X l) \cdot_{R} C (l)$
22	21	adantr	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0})) = (I X l) \cdot_{R} C (l)$
23	22	adantr	$⊢ ((J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \land l \in N) \to if (J = K, (I X l) \cdot_{R} C (l), if (J = l, I X l, \underset{˙}{0})) = (I X l) \cdot_{R} C (l)$
24	20 23	eqtrd	$⊢ ((J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \land l \in N) \to (I X l) \cdot_{R} (l E J) = (I X l) \cdot_{R} C (l)$
25	24	mpteq2dva	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to (l \in N ⟼ (I X l) \cdot_{R} (l E J)) = (l \in N ⟼ (I X l) \cdot_{R} C (l))$
26	25	oveq2d	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} C (l))$
27		fveq1	$⊢ X \underset{˙}{\times} C = Z \to (X \underset{˙}{\times} C) (I) = Z (I)$
28	27	eqcomd	$⊢ X \underset{˙}{\times} C = Z \to Z (I) = (X \underset{˙}{\times} C) (I)$
29	28	3ad2ant3	$⊢ (I \in N \land J \in N \land X \underset{˙}{\times} C = Z) \to Z (I) = (X \underset{˙}{\times} C) (I)$
30	29	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 X \underset{˙}{\times} C = Z)) \to Z (I) = (X \underset{˙}{\times} C) (I)$
31	30	adantl	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to Z (I) = (X \underset{˙}{\times} C) (I)$
32		eqid	$⊢ {Base}_{R} = {Base}_{R}$
33		eqid	$⊢ \cdot_{R} = \cdot_{R}$
34	8	adantl	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to R \in Ring$
35	1 2	matrcl	$⊢ X \in B \to (N \in Fin \land R \in V)$
36	35	simpld	$⊢ X \in B \to N \in Fin$
37	36	3ad2ant1	$⊢ (X \in B \land C \in V \land K \in N) \to N \in Fin$
38	37	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 X \underset{˙}{\times} C = Z)) \to N \in Fin$
39	38	adantl	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to N \in Fin$
40	2	eleq2i	$⊢ X \in B \leftrightarrow X \in {Base}_{A}$
41	40	biimpi	$⊢ X \in B \to X \in {Base}_{A}$
42	41	3ad2ant1	$⊢ (X \in B \land C \in V \land K \in N) \to X \in {Base}_{A}$
43	42	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 X \underset{˙}{\times} C = Z)) \to X \in {Base}_{A}$
44	43	adantl	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to X \in {Base}_{A}$
45	3	eleq2i	$⊢ C \in V \leftrightarrow C \in ({Base}_{R}^{N})$
46	45	biimpi	$⊢ C \in V \to C \in ({Base}_{R}^{N})$
47	46	3ad2ant2	$⊢ (X \in B \land C \in V \land K \in N) \to C \in ({Base}_{R}^{N})$
48	47	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 X \underset{˙}{\times} C = Z)) \to C \in ({Base}_{R}^{N})$
49	48	adantl	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to C \in ({Base}_{R}^{N})$
50	12	adantl	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to I \in N$
51	1 7 32 33 34 39 44 49 50	mavmulfv	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to (X \underset{˙}{\times} C) (I) = \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} C (l))$
52	31 51	eqtrd	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to Z (I) = \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} C (l))$
53		iftrue	$⊢ J = K \to if (J = K, Z (I), I X J) = Z (I)$
54	53	eqcomd	$⊢ J = K \to Z (I) = if (J = K, Z (I), I X J)$
55	54	adantr	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to Z (I) = if (J = K, Z (I), I X J)$
56	26 52 55	3eqtr2d	$⊢ (J = K \land (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z))) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = if (J = K, Z (I), I X J)$
57	56	ex	$⊢ J = K \to ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = if (J = K, Z (I), I X J))$
58	8	adantr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land J \neq K) \to R \in Ring$
59		simpl2	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land J \neq K) \to (X \in B \land C \in V \land K \in N)$
60	12	adantr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land J \neq K) \to I \in N$
61		simpl32	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land J \neq K) \to J \in N$
62		simpr	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land J \neq K) \to J \neq K$
63	1 2 3 4 5 6	mulmarep1gsum1	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land J \neq K)) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = I X J$
64	58 59 60 61 62 63	syl113anc	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land J \neq K) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = I X J$
65		df-ne	$⊢ J \neq K \leftrightarrow \neg J = K$
66		iffalse	$⊢ \neg J = K \to if (J = K, Z (I), I X J) = I X J$
67	66	eqcomd	$⊢ \neg J = K \to I X J = if (J = K, Z (I), I X J)$
68	65 67	sylbi	$⊢ J \neq K \to I X J = if (J = K, Z (I), I X J)$
69	68	adantl	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land J \neq K) \to I X J = if (J = K, Z (I), I X J)$
70	64 69	eqtrd	$⊢ ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \land J \neq K) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = if (J = K, Z (I), I X J)$
71	70	expcom	$⊢ J \neq K \to ((R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = if (J = K, Z (I), I X J))$
72	57 71	pm2.61ine	$⊢ (R \in Ring \land (X \in B \land C \in V \land K \in N) \land (I \in N \land J \in N \land X \underset{˙}{\times} C = Z)) \to \underset{l \in N}{\sum_{R}} ((I X l) \cdot_{R} (l E J)) = if (J = K, Z (I), I X J)$

Metamath Proof Explorer

Theorem mulmarep1gsum2

Proof