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	birani	$⊢ (x \in B \land y \in B) \to x \in {Base}_{A}$
18	17	adantl	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to x \in {Base}_{A}$
19	2 11	matbas2	$⊢ (N \in Fin \land R \in CRing) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
20	19	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to {Base}_{R}^{(N \times N)} = {Base}_{A}$
21	18 20	eleqtrrd	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to x \in ({Base}_{R}^{(N \times N)})$
22	3	eleq2i	$⊢ y \in B \leftrightarrow y \in {Base}_{A}$
23	22	biimpi	$⊢ y \in B \to y \in {Base}_{A}$
24	23	ad2antll	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to y \in {Base}_{A}$
25	19	eleq2d	$⊢ (N \in Fin \land R \in CRing) \to (y \in ({Base}_{R}^{(N \times N)}) \leftrightarrow y \in {Base}_{A})$
26	25	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})$
27	24 26	mpbird	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to y \in ({Base}_{R}^{(N \times N)})$
28	7 11 12 14 15 15 15 21 27	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)))$
29	10 28	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)))$
30	29	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)))$
31		oveq1	$⊢ i = k \to i x m = k x m$
32		oveq2	$⊢ j = l \to m y j = m y l$
33	31 32	oveqan12d	$⊢ (i = k \land j = l) \to (i x m) \cdot_{R} (m y j) = (k x m) \cdot_{R} (m y l)$
34	33	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))$
35	34	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))$
36	35	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))$
37		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$
38		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$
39		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$
40	30 36 37 38 39	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))$
41	40	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)))$
42		eqid	$⊢ 0_{R} = 0_{R}$
43		ringcmn	$⊢ R \in Ring \to R \in CMnd$
44	13 43	syl	$⊢ R \in CRing \to R \in CMnd$
45	44	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to R \in CMnd$
46	45	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$
47	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
48	13 47	syl	$⊢ R \in CRing \to P \in Ring$
49		ringmnd	$⊢ P \in Ring \to P \in Mnd$
50	48 49	syl	$⊢ R \in CRing \to P \in Mnd$
51	50	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to P \in Mnd$
52	51	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$
53	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$
54		eqid	$⊢ algSc (P) = algSc (P)$
55		eqid	$⊢ Scalar (P) = Scalar (P)$
56	48	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in Ring$
57	4	ply1lmod	$⊢ R \in Ring \to P \in LMod$
58	13 57	syl	$⊢ R \in CRing \to P \in LMod$
59	58	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in LMod$
60	54 55 56 59	asclghm	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (Scalar (P) GrpHom P)$
61	4	ply1sca	$⊢ R \in CRing \to R = Scalar (P)$
62	61	adantl	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (P)$
63	62	oveq1d	$⊢ (N \in Fin \land R \in CRing) \to R GrpHom P = Scalar (P) GrpHom P$
64	60 63	eleqtrrd	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (R GrpHom P)$
65		ghmmhm	$⊢ algSc (P) \in (R GrpHom P) \to algSc (P) \in (R MndHom P)$
66	64 65	syl	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (R MndHom P)$
67	66	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to algSc (P) \in (R MndHom P)$
68	67	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)$
69	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$
70	69	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$
71	37	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$
72		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$
73	18	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}$
74	73	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}$
75	74 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$
76	2 11 3 71 72 75	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}$
77	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 l \in N$
78	2	fveq2i	$⊢ {Base}_{A} = {Base}_{(N Mat R)}$
79	3 78	eqtri	$⊢ B = {Base}_{(N Mat R)}$
80	79	eleq2i	$⊢ y \in B \leftrightarrow y \in {Base}_{(N Mat R)}$
81	80	biimpi	$⊢ y \in B \to y \in {Base}_{(N Mat R)}$
82	81	ad2antll	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to y \in {Base}_{(N Mat R)}$
83	82	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)}$
84	83	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)}$
85	84 80	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$
86	2 11 3 72 77 85	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}$
87	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}$
88	70 76 86 87	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}$
89		eqid	$⊢ (m \in N ⟼ (k x m) \cdot_{R} (m y l)) = (m \in N ⟼ (k x m) \cdot_{R} (m y l))$
90		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$
91		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$
92	89 53 90 91	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)))$
93	11 42 46 52 53 68 88 92	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)))$
94	4	ply1assa	$⊢ R \in CRing \to P \in AssAlg$
95	94	adantl	$⊢ (N \in Fin \land R \in CRing) \to P \in AssAlg$
96	54 55	asclrhm	$⊢ P \in AssAlg \to algSc (P) \in (Scalar (P) RingHom P)$
97	95 96	syl	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (Scalar (P) RingHom P)$
98	62	oveq1d	$⊢ (N \in Fin \land R \in CRing) \to R RingHom P = Scalar (P) RingHom P$
99	97 98	eleqtrrd	$⊢ (N \in Fin \land R \in CRing) \to algSc (P) \in (R RingHom P)$
100	99	adantr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to algSc (P) \in (R RingHom P)$
101	100	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)$
102	101	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)$
103	24	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}$
104	103	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}$
105	104 22	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$
106	2 11 3 72 77 105	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}$
107		eqid	$⊢ \cdot_{P} = \cdot_{P}$
108	11 12 107	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)$
109	102 76 106 108	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)$
110	109	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))$
111	110	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))$
112	41 93 111	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))$
113	112	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)))$
114		eqid	$⊢ {Base}_{P} = {Base}_{P}$
115		eqid	$⊢ \cdot_{C} = \cdot_{C}$
116	48	ad2antlr	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to P \in Ring$
117		eqid	$⊢ (i \in N, j \in N ⟼ algSc (P) (i x j)) = (i \in N, j \in N ⟼ algSc (P) (i x j))$
118		eqid	$⊢ (i \in N, j \in N ⟼ algSc (P) (i y j)) = (i \in N, j \in N ⟼ algSc (P) (i y j))$
119	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$
120		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$
121		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$
122		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$
123	2 11 3 120 121 122	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}$
124	4 54 11 114	ply1sclcl	$⊢ (R \in Ring \land i x j \in {Base}_{R}) \to algSc (P) (i x j) \in {Base}_{P}$
125	119 123 124	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}$
126		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$
127	2 11 3 120 121 126	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}$
128	4 54 11 114	ply1sclcl	$⊢ (R \in Ring \land i y j \in {Base}_{R}) \to algSc (P) (i y j) \in {Base}_{P}$
129	119 127 128	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}$
130		oveq12	$⊢ (k = i \land m = j) \to k x m = i x j$
131	130	fveq2d	$⊢ (k = i \land m = j) \to algSc (P) (k x m) = algSc (P) (i x j)$
132	131	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)$
133		oveq12	$⊢ (m = i \land l = j) \to m y l = i y j$
134	133	fveq2d	$⊢ (m = i \land l = j) \to algSc (P) (m y l) = algSc (P) (i y j)$
135	134	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)$
136		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$
137		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$
138	5 114 115 107 116 15 117 118 125 129 132 135 136 137	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)))$
139	113 138	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))$
140	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
141	13 140	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
142	141	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))$
143		3anass	$⊢ (A \in Ring \land x \in B \land y \in B) \leftrightarrow (A \in Ring \land (x \in B \land y \in B))$
144	142 143	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)$
145		eqid	$⊢ \cdot_{A} = \cdot_{A}$
146	3 145	ringcl	$⊢ (A \in Ring \land x \in B \land y \in B) \to x \cdot_{A} y \in B$
147	144 146	syl	$⊢ ((N \in Fin \land R \in CRing) \land (x \in B \land y \in B)) \to x \cdot_{A} y \in B$
148	1 2 3 4 54	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))$
149	15 14 147 148	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))$
150		simpl	$⊢ (x \in B \land y \in B) \to x \in B$
151	150	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)$
152		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)$
153	151 152	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)$
154	1 2 3 4 54	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))$
155	153 154	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))$
156		simpr	$⊢ (x \in B \land y \in B) \to y \in B$
157	156	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)$
158		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)$
159	157 158	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)$
160	1 2 3 4 54	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))$
161	159 160	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))$
162	155 161	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))$
163	139 149 162	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)$
164	163	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