decpmatmullem

Description: Lemma for decpmatmul . (Contributed by AV, 20-Oct-2019) (Revised by AV, 3-Dec-2019)

	Ref	Expression
Hypotheses	decpmatmul.p	$⊢ P = {Poly}_{1} (R)$
	decpmatmul.c	$⊢ C = N Mat P$
	decpmatmul.b	$⊢ B = {Base}_{C}$
Assertion	decpmatmullem	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to I ((U \cdot_{C} W) decompPMat K) J = \underset{t \in N}{\sum_{R}} ({\sum_{R}}_{l = 0}^{K}, ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l)))$

Proof

Step	Hyp	Ref	Expression
1		decpmatmul.p	$⊢ P = {Poly}_{1} (R)$
2		decpmatmul.c	$⊢ C = N Mat P$
3		decpmatmul.b	$⊢ B = {Base}_{C}$
4		simpr	$⊢ (N \in Fin \land R \in Ring) \to R \in Ring$
5	4	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to R \in Ring$
6	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
7	6	adantr	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B)) \to C \in Ring$
8		simpl	$⊢ (U \in B \land W \in B) \to U \in B$
9	8	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B)) \to U \in B$
10		simpr	$⊢ (U \in B \land W \in B) \to W \in B$
11	10	adantl	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B)) \to W \in B$
12		eqid	$⊢ \cdot_{C} = \cdot_{C}$
13	3 12	ringcl	$⊢ (C \in Ring \land U \in B \land W \in B) \to U \cdot_{C} W \in B$
14	7 9 11 13	syl3anc	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B)) \to U \cdot_{C} W \in B$
15	14	3adant3	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to U \cdot_{C} W \in B$
16		simp33	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to K \in ℕ_{0}$
17		3simpa	$⊢ (I \in N \land J \in N \land K \in ℕ_{0}) \to (I \in N \land J \in N)$
18	17	3ad2ant3	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to (I \in N \land J \in N)$
19	1 2 3	decpmate	$⊢ ((R \in Ring \land U \cdot_{C} W \in B \land K \in ℕ_{0}) \land (I \in N \land J \in N)) \to I ((U \cdot_{C} W) decompPMat K) J = {coe}_{1} (I (U \cdot_{C} W) J) (K)$
20	5 15 16 18 19	syl31anc	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to I ((U \cdot_{C} W) decompPMat K) J = {coe}_{1} (I (U \cdot_{C} W) J) (K)$
21	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
22		eqid	$⊢ P maMul ⟨N, N, N⟩ = P maMul ⟨N, N, N⟩$
23	2 22	matmulr	$⊢ (N \in Fin \land P \in Ring) \to P maMul ⟨N, N, N⟩ = \cdot_{C}$
24	23	eqcomd	$⊢ (N \in Fin \land P \in Ring) \to \cdot_{C} = P maMul ⟨N, N, N⟩$
25	21 24	sylan2	$⊢ (N \in Fin \land R \in Ring) \to \cdot_{C} = P maMul ⟨N, N, N⟩$
26	25	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to \cdot_{C} = P maMul ⟨N, N, N⟩$
27	26	oveqd	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to U \cdot_{C} W = U (P maMul ⟨N, N, N⟩) W$
28	27	oveqd	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to I (U \cdot_{C} W) J = I (U (P maMul ⟨N, N, N⟩) W) J$
29		eqid	$⊢ {Base}_{P} = {Base}_{P}$
30		eqid	$⊢ \cdot_{P} = \cdot_{P}$
31	21	adantl	$⊢ (N \in Fin \land R \in Ring) \to P \in Ring$
32	31	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to P \in Ring$
33		simpl	$⊢ (N \in Fin \land R \in Ring) \to N \in Fin$
34	33	3ad2ant1	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to N \in Fin$
35	2 29	matbas2	$⊢ (N \in Fin \land P \in Ring) \to {Base}_{P}^{(N \times N)} = {Base}_{C}$
36	3 35	eqtr4id	$⊢ (N \in Fin \land P \in Ring) \to B = {Base}_{P}^{(N \times N)}$
37	21 36	sylan2	$⊢ (N \in Fin \land R \in Ring) \to B = {Base}_{P}^{(N \times N)}$
38	37	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (U \in B \leftrightarrow U \in ({Base}_{P}^{(N \times N)}))$
39	38	biimpcd	$⊢ U \in B \to ((N \in Fin \land R \in Ring) \to U \in ({Base}_{P}^{(N \times N)}))$
40	39	adantr	$⊢ (U \in B \land W \in B) \to ((N \in Fin \land R \in Ring) \to U \in ({Base}_{P}^{(N \times N)}))$
41	40	impcom	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B)) \to U \in ({Base}_{P}^{(N \times N)})$
42	41	3adant3	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to U \in ({Base}_{P}^{(N \times N)})$
43	21 35	sylan2	$⊢ (N \in Fin \land R \in Ring) \to {Base}_{P}^{(N \times N)} = {Base}_{C}$
44	3 43	eqtr4id	$⊢ (N \in Fin \land R \in Ring) \to B = {Base}_{P}^{(N \times N)}$
45	44	eleq2d	$⊢ (N \in Fin \land R \in Ring) \to (W \in B \leftrightarrow W \in ({Base}_{P}^{(N \times N)}))$
46	45	biimpcd	$⊢ W \in B \to ((N \in Fin \land R \in Ring) \to W \in ({Base}_{P}^{(N \times N)}))$
47	46	adantl	$⊢ (U \in B \land W \in B) \to ((N \in Fin \land R \in Ring) \to W \in ({Base}_{P}^{(N \times N)}))$
48	47	impcom	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B)) \to W \in ({Base}_{P}^{(N \times N)})$
49	48	3adant3	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to W \in ({Base}_{P}^{(N \times N)})$
50		simp31	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to I \in N$
51		simp32	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to J \in N$
52	22 29 30 32 34 34 34 42 49 50 51	mamufv	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to I (U (P maMul ⟨N, N, N⟩) W) J = \underset{t \in N}{\sum_{P}} ((I U t) \cdot_{P} (t W J))$
53	28 52	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to I (U \cdot_{C} W) J = \underset{t \in N}{\sum_{P}} ((I U t) \cdot_{P} (t W J))$
54	53	fveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to {coe}_{1} (I (U \cdot_{C} W) J) = {coe}_{1} (\underset{t \in N}{\sum_{P}} ((I U t) \cdot_{P} (t W J)))$
55	54	fveq1d	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to {coe}_{1} (I (U \cdot_{C} W) J) (K) = {coe}_{1} (\underset{t \in N}{\sum_{P}} ((I U t) \cdot_{P} (t W J))) (K)$
56	32	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to P \in Ring$
57	50	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to I \in N$
58		simpr	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to t \in N$
59		simpl2l	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to U \in B$
60	2 29 3 57 58 59	matecld	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to I U t \in {Base}_{P}$
61	51	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to J \in N$
62		simpl2r	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to W \in B$
63	2 29 3 58 61 62	matecld	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to t W J \in {Base}_{P}$
64	29 30	ringcl	$⊢ (P \in Ring \land I U t \in {Base}_{P} \land t W J \in {Base}_{P}) \to (I U t) \cdot_{P} (t W J) \in {Base}_{P}$
65	56 60 63 64	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to (I U t) \cdot_{P} (t W J) \in {Base}_{P}$
66	65	ralrimiva	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to \forall t \in N (I U t) \cdot_{P} (t W J) \in {Base}_{P}$
67	1 29 5 16 66 34	coe1fzgsumd	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to {coe}_{1} (\underset{t \in N}{\sum_{P}} ((I U t) \cdot_{P} (t W J))) (K) = \underset{t \in N}{\sum_{R}} {coe}_{1} ((I U t) \cdot_{P} (t W J)) (K)$
68		simpl1r	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to R \in Ring$
69		eqid	$⊢ \cdot_{R} = \cdot_{R}$
70	1 30 69 29	coe1mul	$⊢ (R \in Ring \land I U t \in {Base}_{P} \land t W J \in {Base}_{P}) \to {coe}_{1} ((I U t) \cdot_{P} (t W J)) = (k \in ℕ_{0} ⟼ {\sum_{R}}_{l = 0}^{k} ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (k - l)))$
71	68 60 63 70	syl3anc	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to {coe}_{1} ((I U t) \cdot_{P} (t W J)) = (k \in ℕ_{0} ⟼ {\sum_{R}}_{l = 0}^{k} ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (k - l)))$
72		oveq2	$⊢ k = K \to (0 \dots k) = (0 \dots K)$
73		fvoveq1	$⊢ k = K \to {coe}_{1} (t W J) (k - l) = {coe}_{1} (t W J) (K - l)$
74	73	oveq2d	$⊢ k = K \to {coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (k - l) = {coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l)$
75	72 74	mpteq12dv	$⊢ k = K \to (l \in (0 \dots k) ⟼ {coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (k - l)) = (l \in (0 \dots K) ⟼ {coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l))$
76	75	oveq2d	$⊢ k = K \to {\sum_{R}}_{l = 0}^{k} ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (k - l)) = {\sum_{R}}_{l = 0}^{K} ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l))$
77	76	adantl	$⊢ ((((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \land k = K) \to {\sum_{R}}_{l = 0}^{k} ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (k - l)) = {\sum_{R}}_{l = 0}^{K} ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l))$
78	16	adantr	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to K \in ℕ_{0}$
79		ovexd	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to {\sum_{R}}_{l = 0}^{K} ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l)) \in V$
80	71 77 78 79	fvmptd	$⊢ (((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \land t \in N) \to {coe}_{1} ((I U t) \cdot_{P} (t W J)) (K) = {\sum_{R}}_{l = 0}^{K} ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l))$
81	80	mpteq2dva	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to (t \in N ⟼ {coe}_{1} ((I U t) \cdot_{P} (t W J)) (K)) = (t \in N ⟼ {\sum_{R}}_{l = 0}^{K} ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l)))$
82	81	oveq2d	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to \underset{t \in N}{\sum_{R}} {coe}_{1} ((I U t) \cdot_{P} (t W J)) (K) = \underset{t \in N}{\sum_{R}} ({\sum_{R}}_{l = 0}^{K}, ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l)))$
83	67 82	eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to {coe}_{1} (\underset{t \in N}{\sum_{P}} ((I U t) \cdot_{P} (t W J))) (K) = \underset{t \in N}{\sum_{R}} ({\sum_{R}}_{l = 0}^{K}, ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l)))$
84	20 55 83	3eqtrd	$⊢ ((N \in Fin \land R \in Ring) \land (U \in B \land W \in B) \land (I \in N \land J \in N \land K \in ℕ_{0})) \to I ((U \cdot_{C} W) decompPMat K) J = \underset{t \in N}{\sum_{R}} ({\sum_{R}}_{l = 0}^{K}, ({coe}_{1} (I U t) (l) \cdot_{R} {coe}_{1} (t W J) (K - l)))$

Metamath Proof Explorer

Theorem decpmatmullem

Proof