pmatcollpwlem

Description: Lemma for pmatcollpw . (Contributed by AV, 26-Oct-2019) (Revised by AV, 4-Dec-2019)

	Ref	Expression
Hypotheses	pmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
	pmatcollpw.c	$⊢ C = N Mat P$
	pmatcollpw.b	$⊢ B = {Base}_{C}$
	pmatcollpw.m	$⊢ \underset{˙}{*} = \cdot_{C}$
	pmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	pmatcollpw.x	$⊢ X = {var}_{1} (R)$
	pmatcollpw.t	$⊢ T = N matToPolyMat R$
Assertion	pmatcollpwlem	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X) = a ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)) b$

Proof

Step	Hyp	Ref	Expression
1		pmatcollpw.p	$⊢ P = {Poly}_{1} (R)$
2		pmatcollpw.c	$⊢ C = N Mat P$
3		pmatcollpw.b	$⊢ B = {Base}_{C}$
4		pmatcollpw.m	$⊢ \underset{˙}{*} = \cdot_{C}$
5		pmatcollpw.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
6		pmatcollpw.x	$⊢ X = {var}_{1} (R)$
7		pmatcollpw.t	$⊢ T = N matToPolyMat R$
8	1	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
9	8	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in AssAlg$
10	9	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to P \in AssAlg$
11	10	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to P \in AssAlg$
12		eqid	$⊢ N Mat R = N Mat R$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
15		simp2	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to a \in N$
16		simp3	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to b \in N$
17		simp2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in CRing$
18	17	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to R \in CRing$
19		simp3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to M \in B$
20	19	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to M \in B$
21		simpr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
22	1 2 3 12 14	decpmatcl	$⊢ (R \in CRing \land M \in B \land n \in ℕ_{0}) \to M decompPMat n \in {Base}_{(N Mat R)}$
23	18 20 21 22	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to M decompPMat n \in {Base}_{(N Mat R)}$
24	23	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to M decompPMat n \in {Base}_{(N Mat R)}$
25	12 13 14 15 16 24	matecld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to a (M decompPMat n) b \in {Base}_{R}$
26		crngring	$⊢ R \in CRing \to R \in Ring$
27	26	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R \in Ring$
28	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
29	27 28	syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R = Scalar (P)$
30	29	eqcomd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to Scalar (P) = R$
31	30	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (P)} = {Base}_{R}$
32	31	eleq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (a (M decompPMat n) b \in {Base}_{Scalar (P)} \leftrightarrow a (M decompPMat n) b \in {Base}_{R})$
33	32	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (a (M decompPMat n) b \in {Base}_{Scalar (P)} \leftrightarrow a (M decompPMat n) b \in {Base}_{R})$
34	33	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (a (M decompPMat n) b \in {Base}_{Scalar (P)} \leftrightarrow a (M decompPMat n) b \in {Base}_{R})$
35	25 34	mpbird	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to a (M decompPMat n) b \in {Base}_{Scalar (P)}$
36		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
37		eqid	$⊢ {Base}_{P} = {Base}_{P}$
38	1 6 36 5 37	ply1moncl	$⊢ (R \in Ring \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in {Base}_{P}$
39	27 38	sylan	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to n \underset{˙}{\times} X \in {Base}_{P}$
40	39	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to n \underset{˙}{\times} X \in {Base}_{P}$
41		eqid	$⊢ algSc (P) = algSc (P)$
42		eqid	$⊢ Scalar (P) = Scalar (P)$
43		eqid	$⊢ {Base}_{Scalar (P)} = {Base}_{Scalar (P)}$
44		eqid	$⊢ \cdot_{P} = \cdot_{P}$
45		eqid	$⊢ \cdot_{P} = \cdot_{P}$
46	41 42 43 37 44 45	asclmul2	$⊢ (P \in AssAlg \land a (M decompPMat n) b \in {Base}_{Scalar (P)} \land n \underset{˙}{\times} X \in {Base}_{P}) \to (n \underset{˙}{\times} X) \cdot_{P} algSc (P) (a (M decompPMat n) b) = (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X)$
47	11 35 40 46	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (n \underset{˙}{\times} X) \cdot_{P} algSc (P) (a (M decompPMat n) b) = (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X)$
48		eqidd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) = (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j))$
49		oveq12	$⊢ (i = a \land j = b) \to i (M decompPMat n) j = a (M decompPMat n) b$
50	49	fveq2d	$⊢ (i = a \land j = b) \to algSc (P) (i (M decompPMat n) j) = algSc (P) (a (M decompPMat n) b)$
51	50	adantl	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \land (i = a \land j = b)) \to algSc (P) (i (M decompPMat n) j) = algSc (P) (a (M decompPMat n) b)$
52		fvexd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to algSc (P) (a (M decompPMat n) b) \in V$
53	48 51 15 16 52	ovmpod	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to a (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) b = algSc (P) (a (M decompPMat n) b)$
54	53	eqcomd	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to algSc (P) (a (M decompPMat n) b) = a (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) b$
55	54	oveq2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (n \underset{˙}{\times} X) \cdot_{P} algSc (P) (a (M decompPMat n) b) = (n \underset{˙}{\times} X) \cdot_{P} (a (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) b)$
56	47 55	eqtr3d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X) = (n \underset{˙}{\times} X) \cdot_{P} (a (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) b)$
57	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
58	26 57	syl	$⊢ R \in CRing \to P \in Ring$
59	58	3ad2ant2	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to P \in Ring$
60	59	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to P \in Ring$
61	60	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to P \in Ring$
62		simpl1	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to N \in Fin$
63	18 26	syl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to R \in Ring$
64	63	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to R \in Ring$
65		simp2	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to i \in N$
66		simp3	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to j \in N$
67	23	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to M decompPMat n \in {Base}_{(N Mat R)}$
68	12 13 14 65 66 67	matecld	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to i (M decompPMat n) j \in {Base}_{R}$
69	1 41 13 37	ply1sclcl	$⊢ (R \in Ring \land i (M decompPMat n) j \in {Base}_{R}) \to algSc (P) (i (M decompPMat n) j) \in {Base}_{P}$
70	64 68 69	syl2anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land i \in N \land j \in N) \to algSc (P) (i (M decompPMat n) j) \in {Base}_{P}$
71	2 37 3 62 60 70	matbas2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) \in B$
72	39 71	jca	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (n \underset{˙}{\times} X \in {Base}_{P} \land (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) \in B)$
73	72	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (n \underset{˙}{\times} X \in {Base}_{P} \land (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) \in B)$
74	15 16	jca	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (a \in N \land b \in N)$
75	2 3 37 4 44	matvscacell	$⊢ (P \in Ring \land (n \underset{˙}{\times} X \in {Base}_{P} \land (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) \in B) \land (a \in N \land b \in N)) \to a ((n \underset{˙}{\times} X) \underset{˙}{*} (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j))) b = (n \underset{˙}{\times} X) \cdot_{P} (a (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) b)$
76	61 73 74 75	syl3anc	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to a ((n \underset{˙}{\times} X) \underset{˙}{*} (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j))) b = (n \underset{˙}{\times} X) \cdot_{P} (a (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) b)$
77	27	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to R \in Ring$
78	7 12 14 1 41	mat2pmatval	$⊢ (N \in Fin \land R \in Ring \land M decompPMat n \in {Base}_{(N Mat R)}) \to T (M decompPMat n) = (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j))$
79	62 77 23 78	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to T (M decompPMat n) = (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j))$
80	79	eqcomd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) = T (M decompPMat n)$
81	80	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to (n \underset{˙}{\times} X) \underset{˙}{} (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j)) = (n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n)$
82	81	oveqd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \to a ((n \underset{˙}{\times} X) \underset{˙}{} (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j))) b = a ((n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n)) b$
83	82	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to a ((n \underset{˙}{\times} X) \underset{˙}{} (i \in N, j \in N ⟼ algSc (P) (i (M decompPMat n) j))) b = a ((n \underset{˙}{\times} X) \underset{˙}{} T (M decompPMat n)) b$
84	56 76 83	3eqtr2d	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land n \in ℕ_{0}) \land a \in N \land b \in N) \to (a (M decompPMat n) b) \cdot_{P} (n \underset{˙}{\times} X) = a ((n \underset{˙}{\times} X) \underset{˙}{*} T (M decompPMat n)) b$

Metamath Proof Explorer

Theorem pmatcollpwlem

Proof