mat2pmatmul

Description: The transformation of matrices into polynomial matrices preserves the multiplication. (Contributed by AV, 29-Oct-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	mat2pmatbas.t	$⊢ T = N matToPolyMat R$
	mat2pmatbas.a	$⊢ A = N Mat R$
	mat2pmatbas.b	$⊢ B = {Base}_{A}$
	mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
	mat2pmatbas.c	$⊢ C = N Mat P$
	mat2pmatbas0.h	$⊢ H = {Base}_{C}$
Assertion	mat2pmatmul	$⊢ (N \in Fin \land R \in CRing) \to \forall x \in B \forall y \in B T (x \cdot_{A} y) = T (x) \cdot_{C} T (y)$

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	$⊢ T = N matToPolyMat R$
2		mat2pmatbas.a	$⊢ A = N Mat R$
3		mat2pmatbas.b	$⊢ B = {Base}_{A}$
4		mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
5		mat2pmatbas.c	$⊢ C = N Mat P$
6		mat2pmatbas0.h	$⊢ H = {Base}_{C}$
7		eqid	$⊢ R maMul ⟨N, N, N⟩ = R maMul ⟨N, N, N⟩$
8	2 7	matmulr	$⊢ (N \in Fin \land R \in CRing) \to R maMul ⟨N, N, N⟩ = \cdot_{A}$
9	8	eqcomd	$⊢ (N \in Fin \land R \in CRing) \to \cdot_{A} = R maMul ⟨N, N, N⟩$
10	9	oveqdr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to x \cdot_{A} y = x (R maMul ⟨N, N, N⟩) y$
11		eqid	$⊢ {Base}_{R} = {Base}_{R}$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14	13	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to R \in Ring$
15		simpll	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to N \in Fin$
16	3	eleq2i	$⊢ x \in B \leftrightarrow x \in {Base}_{A}$
17	16	biimpi	$⊢ x \in B \to x \in {Base}_{A}$
18	17	adantr	$⊢ (x \in B \land y \in B) \to x \in {Base}_{A}$
19	18	adantl	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to x \in {Base}_{A}$
20	2 11	matbas2	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
21	20	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
22	19 21	eleqtrrd	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to x \in ({Base}_{R}^{(N \times N)})$
23	3	eleq2i	$⊢ y \in B \leftrightarrow y \in {Base}_{A}$
24	23	biimpi	$⊢ y \in B \to y \in {Base}_{A}$
25	24	ad2antll	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to y \in {Base}_{A}$
26	20	eleq2d	$⊢ (N \in Fin \land R \in CRing) \to (y \in ({Base}_{R}^{(N \times N)}) \leftrightarrow y \in {Base}_{A})$
27	26	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to (y \in ({Base}_{R}^{(N \times N)}) \leftrightarrow y \in {Base}_{A})$
28	25 27	mpbird	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to y \in ({Base}_{R}^{(N \times N)})$
29	7 11 12 14 15 15 15 22 28	mamuval	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to x (R maMul ⟨N, N, N⟩) y = (i \in N, j \in N ⟼ \underset{m \in N}{\sum_{R}} ((i x m) \cdot_{R} (m y j)))$
30	10 29	eqtrd	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to x \cdot_{A} y = (i \in N, j \in N ⟼ \underset{m \in N}{\sum_{R}} ((i x m) \cdot_{R} (m y j)))$
31	30	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to x \cdot_{A} y = (i \in N, j \in N ⟼ \underset{m \in N}{\sum_{R}} ((i x m) \cdot_{R} (m y j)))$
32		oveq1	$⊢ i = k \to i x m = k x m$
33		oveq2	$⊢ j = l \to m y j = m y l$
34	32 33	oveqan12d	$⊢ (i = k \land j = l) \to (i x m) \cdot_{R} (m y j) = (k x m) \cdot_{R} (m y l)$
35	34	mpteq2dv	$⊢ (i = k \land j = l) \to (m \in N ⟼ (i x m) \cdot_{R} (m y j)) = (m \in N ⟼ (k x m) \cdot_{R} (m y l))$
36	35	oveq2d	$⊢ (i = k \land j = l) \to \underset{m \in N}{\sum_{R}} ((i x m) \cdot_{R} (m y j)) = \underset{m \in N}{\sum_{R}} ((k x m) \cdot_{R} (m y l))$
37	36	adantl	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land (i = k \land j = l)) \to \underset{m \in N}{\sum_{R}} ((i x m) \cdot_{R} (m y j)) = \underset{m \in N}{\sum_{R}} ((k x m) \cdot_{R} (m y l))$
38		simp2	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to k \in N$
39		simp3	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to l \in N$
40		ovexd	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to \underset{m \in N}{\sum_{R}} ((k x m) \cdot_{R} (m y l)) \in V$
41	31 37 38 39 40	ovmpod	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to k (x \cdot_{A} y) l = \underset{m \in N}{\sum_{R}} ((k x m) \cdot_{R} (m y l))$
42	41	fveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to algSc (P) (k (x \cdot_{A} y) l) = algSc (P) (\underset{m \in N}{\sum_{R}} ((k x m) \cdot_{R} (m y l)))$
43		eqid	$⊢ 0_{R} = 0_{R}$
44		ringcmn	$⊢ R \in Ring \to R \in CMnd$
45	13 44	syl	$⊢ R \in CRing \to R \in CMnd$
46	45	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to R \in CMnd$
47	46	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to R \in CMnd$
48	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
49	13 48	syl	$⊢ R \in CRing \to P \in Ring$
50		ringmnd	$⊢ P \in Ring \to P \in Mnd$
51	49 50	syl	$⊢ R \in CRing \to P \in Mnd$
52	51	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to P \in Mnd$
53	52	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to P \in Mnd$
54	15	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to N \in Fin$
55		eqid	$⊢ algSc (P) = algSc (P)$
56		eqid	$⊢ Scalar (P) = Scalar (P)$
57	49	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in Ring$
58	4	ply1lmod	$⊢ R \in Ring \to P \in LMod$
59	13 58	syl	$⊢ R \in CRing \to P \in LMod$
60	59	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in LMod$
61	55 56 57 60	asclghm	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (Scalar (P) GrpHom P)$
62	4	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
63	62	adantl	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (P)$
64	63	oveq1d	$⊢ (N \in Fin \land R \in CRing) \to R GrpHom P = Scalar (P) GrpHom P$
65	61 64	eleqtrrd	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (R GrpHom P)$
66		ghmmhm	$⊢ algSc (P) \in (R GrpHom P) \to algSc (P) \in (R MndHom P)$
67	65 66	syl	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (R MndHom P)$
68	67	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to algSc (P) \in (R MndHom P)$
69	68	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to algSc (P) \in (R MndHom P)$
70	14	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to R \in Ring$
71	70	adantr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to R \in Ring$
72	38	adantr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to k \in N$
73		simpr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to m \in N$
74	19	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to x \in {Base}_{A}$
75	74	adantr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to x \in {Base}_{A}$
76	75 16	sylibr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to x \in B$
77	2 11 3 72 73 76	matecld	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to k x m \in {Base}_{R}$
78	39	adantr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to l \in N$
79	2	fveq2i	$⊢ {Base}_{A} = {Base}_{(N Mat R)}$
80	3 79	eqtri	$⊢ B = {Base}_{(N Mat R)}$
81	80	eleq2i	$⊢ y \in B \leftrightarrow y \in {Base}_{(N Mat R)}$
82	81	biimpi	$⊢ y \in B \to y \in {Base}_{(N Mat R)}$
83	82	ad2antll	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to y \in {Base}_{(N Mat R)}$
84	83	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to y \in {Base}_{(N Mat R)}$
85	84	adantr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to y \in {Base}_{(N Mat R)}$
86	85 81	sylibr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to y \in B$
87	2 11 3 73 78 86	matecld	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to m y l \in {Base}_{R}$
88	11 12	ringcl	$⊢ (R \in Ring \land k x m \in {Base}_{R} \land m y l \in {Base}_{R}) \to (k x m) \cdot_{R} (m y l) \in {Base}_{R}$
89	71 77 87 88	syl3anc	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to (k x m) \cdot_{R} (m y l) \in {Base}_{R}$
90		eqid	$⊢ (m \in N ⟼ (k x m) \cdot_{R} (m y l)) = (m \in N ⟼ (k x m) \cdot_{R} (m y l))$
91		ovexd	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to (k x m) \cdot_{R} (m y l) \in V$
92		fvexd	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to 0_{R} \in V$
93	90 54 91 92	fsuppmptdm	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to {finSupp}_{0_{R}} ((m \in N ⟼ (k x m) \cdot_{R} (m y l)))$
94	11 43 47 53 54 69 89 93	gsummptmhm	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to \underset{m \in N}{\sum_{P}} algSc (P) ((k x m) \cdot_{R} (m y l)) = algSc (P) (\underset{m \in N}{\sum_{R}} ((k x m) \cdot_{R} (m y l)))$
95	4	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
96	95	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in AssAlg$
97	55 56	asclrhm	$⊢ P \in AssAlg \to algSc (P) \in (Scalar (P) RingHom P)$
98	96 97	syl	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (Scalar (P) RingHom P)$
99	63	oveq1d	$⊢ (N \in Fin \land R \in CRing) \to R RingHom P = Scalar (P) RingHom P$
100	98 99	eleqtrrd	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (R RingHom P)$
101	100	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to algSc (P) \in (R RingHom P)$
102	101	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to algSc (P) \in (R RingHom P)$
103	102	adantr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to algSc (P) \in (R RingHom P)$
104	25	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to y \in {Base}_{A}$
105	104	adantr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to y \in {Base}_{A}$
106	105 23	sylibr	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to y \in B$
107	2 11 3 73 78 106	matecld	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to m y l \in {Base}_{R}$
108		eqid	$⊢ \cdot_{P} = \cdot_{P}$
109	11 12 108	rhmmul	$⊢ (algSc (P) \in (R RingHom P) \land k x m \in {Base}_{R} \land m y l \in {Base}_{R}) \to algSc (P) ((k x m) \cdot_{R} (m y l)) = algSc (P) (k x m) \cdot_{P} algSc (P) (m y l)$
110	103 77 107 109	syl3anc	$⊢ ((((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \land m \in N) \to algSc (P) ((k x m) \cdot_{R} (m y l)) = algSc (P) (k x m) \cdot_{P} algSc (P) (m y l)$
111	110	mpteq2dva	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to (m \in N ⟼ algSc (P) ((k x m) \cdot_{R} (m y l))) = (m \in N ⟼ algSc (P) (k x m) \cdot_{P} algSc (P) (m y l))$
112	111	oveq2d	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to \underset{m \in N}{\sum_{P}} algSc (P) ((k x m) \cdot_{R} (m y l)) = \underset{m \in N}{\sum_{P}} (algSc (P) (k x m) \cdot_{P} algSc (P) (m y l))$
113	42 94 112	3eqtr2d	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land l \in N) \to algSc (P) (k (x \cdot_{A} y) l) = \underset{m \in N}{\sum_{P}} (algSc (P) (k x m) \cdot_{P} algSc (P) (m y l))$
114	113	mpoeq3dva	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to (k \in N, l \in N ⟼ algSc (P) (k (x \cdot_{A} y) l)) = (k \in N, l \in N ⟼ \underset{m \in N}{\sum_{P}} (algSc (P) (k x m) \cdot_{P} algSc (P) (m y l)))$
115		eqid	$⊢ {Base}_{P} = {Base}_{P}$
116		eqid	$⊢ \cdot_{C} = \cdot_{C}$
117	49	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to P \in Ring$
118		eqid	$⊢ (i \in N, j \in N ⟼ algSc (P) (i x j)) = (i \in N, j \in N ⟼ algSc (P) (i x j))$
119		eqid	$⊢ (i \in N, j \in N ⟼ algSc (P) (i y j)) = (i \in N, j \in N ⟼ algSc (P) (i y j))$
120	14	3ad2ant1	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to R \in Ring$
121		simp2	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i \in N$
122		simp3	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to j \in N$
123		simp1rl	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to x \in B$
124	2 11 3 121 122 123	matecld	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i x j \in {Base}_{R}$
125	4 55 11 115	ply1sclcl	$⊢ (R \in Ring \land i x j \in {Base}_{R}) \to algSc (P) (i x j) \in {Base}_{P}$
126	120 124 125	syl2anc	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) (i x j) \in {Base}_{P}$
127		simp1rr	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to y \in B$
128	2 11 3 121 122 127	matecld	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to i y j \in {Base}_{R}$
129	4 55 11 115	ply1sclcl	$⊢ (R \in Ring \land i y j \in {Base}_{R}) \to algSc (P) (i y j) \in {Base}_{P}$
130	120 128 129	syl2anc	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land i \in N \land j \in N) \to algSc (P) (i y j) \in {Base}_{P}$
131		oveq12	$⊢ (k = i \land m = j) \to k x m = i x j$
132	131	fveq2d	$⊢ (k = i \land m = j) \to algSc (P) (k x m) = algSc (P) (i x j)$
133	132	adantl	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land (k = i \land m = j)) \to algSc (P) (k x m) = algSc (P) (i x j)$
134		oveq12	$⊢ (m = i \land l = j) \to m y l = i y j$
135	134	fveq2d	$⊢ (m = i \land l = j) \to algSc (P) (m y l) = algSc (P) (i y j)$
136	135	adantl	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land (m = i \land l = j)) \to algSc (P) (m y l) = algSc (P) (i y j)$
137		fvexd	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land k \in N \land m \in N) \to algSc (P) (k x m) \in V$
138		fvexd	$⊢ (((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \land m \in N \land l \in N) \to algSc (P) (m y l) \in V$
139	5 115 116 108 117 15 118 119 126 130 133 136 137 138	mpomatmul	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to (i \in N, j \in N ⟼ algSc (P) (i x j)) \cdot_{C} (i \in N, j \in N ⟼ algSc (P) (i y j)) = (k \in N, l \in N ⟼ \underset{m \in N}{\sum_{P}} (algSc (P) (k x m) \cdot_{P} algSc (P) (m y l)))$
140	114 139	eqtr4d	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to (k \in N, l \in N ⟼ algSc (P) (k (x \cdot_{A} y) l)) = (i \in N, j \in N ⟼ algSc (P) (i x j)) \cdot_{C} (i \in N, j \in N ⟼ algSc (P) (i y j))$
141	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
142	13 141	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
143	142	anim1i	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to (A \in Ring \land (x \in B \land y \in B))$
144		3anass	$⊢ (A \in Ring \land x \in B \land y \in B) \leftrightarrow (A \in Ring \land (x \in B \land y \in B))$
145	143 144	sylibr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to (A \in Ring \land x \in B \land y \in B)$
146		eqid	$⊢ \cdot_{A} = \cdot_{A}$
147	3 146	ringcl	$⊢ (A \in Ring \land x \in B \land y \in B) \to x \cdot_{A} y \in B$
148	145 147	syl	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to x \cdot_{A} y \in B$
149	1 2 3 4 55	mat2pmatval	$⊢ (N \in Fin \land R \in Ring \land x \cdot_{A} y \in B) \to T (x \cdot_{A} y) = (k \in N, l \in N ⟼ algSc (P) (k (x \cdot_{A} y) l))$
150	15 14 148 149	syl3anc	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to T (x \cdot_{A} y) = (k \in N, l \in N ⟼ algSc (P) (k (x \cdot_{A} y) l))$
151		simpl	$⊢ (x \in B \land y \in B) \to x \in B$
152	151	anim2i	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to ((N \in Fin \land R \in CRing) \land x \in B)$
153		df-3an	$⊢ (N \in Fin \land R \in CRing \land x \in B) \leftrightarrow ((N \in Fin \land R \in CRing) \land x \in B)$
154	152 153	sylibr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to (N \in Fin \land R \in CRing \land x \in B)$
155	1 2 3 4 55	mat2pmatval	$⊢ (N \in Fin \land R \in CRing \land x \in B) \to T (x) = (i \in N, j \in N ⟼ algSc (P) (i x j))$
156	154 155	syl	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to T (x) = (i \in N, j \in N ⟼ algSc (P) (i x j))$
157		simpr	$⊢ (x \in B \land y \in B) \to y \in B$
158	157	anim2i	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to ((N \in Fin \land R \in CRing) \land y \in B)$
159		df-3an	$⊢ (N \in Fin \land R \in CRing \land y \in B) \leftrightarrow ((N \in Fin \land R \in CRing) \land y \in B)$
160	158 159	sylibr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to (N \in Fin \land R \in CRing \land y \in B)$
161	1 2 3 4 55	mat2pmatval	$⊢ (N \in Fin \land R \in CRing \land y \in B) \to T (y) = (i \in N, j \in N ⟼ algSc (P) (i y j))$
162	160 161	syl	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to T (y) = (i \in N, j \in N ⟼ algSc (P) (i y j))$
163	156 162	oveq12d	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to T (x) \cdot_{C} T (y) = (i \in N, j \in N ⟼ algSc (P) (i x j)) \cdot_{C} (i \in N, j \in N ⟼ algSc (P) (i y j))$
164	140 150 163	3eqtr4d	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to T (x \cdot_{A} y) = T (x) \cdot_{C} T (y)$
165	164	ralrimivva	$⊢ (N \in Fin \land R \in CRing) \to \forall x \in B \forall y \in B T (x \cdot_{A} y) = T (x) \cdot_{C} T (y)$

Metamath Proof Explorer

Theorem mat2pmatmul

Proof