Theorem mat2pmatmul 22962

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

Hypotheses

Ref	Expression
mat2pmatbas.t	⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
mat2pmatbas.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mat2pmatbas.b	⊢ 𝐵 = (Base‘𝐴)
mat2pmatbas.p	⊢ 𝑃 = (Poly1‘𝑅)
mat2pmatbas.c	⊢ 𝐶 = (𝑁 Mat 𝑃)
mat2pmatbas0.h	⊢ 𝐻 = (Base‘𝐶)

Assertion

Ref	Expression
mat2pmatmul	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐴)𝑦)) = ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦)))

Distinct variable groups:   𝑥,𝐵,𝑦   𝑥,𝑁,𝑦   𝑥,𝑃,𝑦   𝑥,𝑅,𝑦   𝑥,𝑇,𝑦   𝑥,𝐴,𝑦   𝑥,𝐶,𝑦   𝑥,𝐻,𝑦

Proof of Theorem mat2pmatmul

Dummy variables 𝑚 𝑖 𝑗 𝑘 𝑙 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mat2pmatbas.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = (𝑁 Mat 𝑅)
2		eqid 2762	. . . . . . . . . . . . 13 ⊢ (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
3	1, 2	matmulr 22666	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r‘𝐴))
4	3	eqcomd 2768	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (.r‘𝐴) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩))
5	4	oveqdr 7445	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐴)𝑦) = (𝑥(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝑦))
6		eqid 2762	. . . . . . . . . . 11 ⊢ (Base‘𝑅) = (Base‘𝑅)
7		eqid 2762	. . . . . . . . . . 11 ⊢ (.r‘𝑅) = (.r‘𝑅)
8		crngring 20390	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
9	8	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ Ring)
10		simpll 779	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑁 ∈ Fin)
11		mat2pmatbas.b	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘𝐴)
12	11	eleq2i 2854	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐴))
13	12	birani 509	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ (Base‘𝐴))
14	13	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ (Base‘𝐴))
15	1, 6	matbas2 22649	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = (Base‘𝐴))
16	15	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((Base‘𝑅) ↑m (𝑁 × 𝑁)) = (Base‘𝐴))
17	14, 16	eleqtrrd 2865	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
18	11	eleq2i 2854	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘𝐴))
19	18	biimpi 219	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (Base‘𝐴))
20	19	ad2antll 742	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (Base‘𝐴))
21	15	eleq2d 2848	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ↔ 𝑦 ∈ (Base‘𝐴)))
22	21	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)) ↔ 𝑦 ∈ (Base‘𝐴)))
23	20, 22	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ ((Base‘𝑅) ↑m (𝑁 × 𝑁)))
24	2, 6, 7, 9, 10, 10, 10, 17, 23	mamuval 22621	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗))))))
25	5, 24	eqtrd 2797	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐴)𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗))))))
26	25	3ad2ant1 1151	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑥(.r‘𝐴)𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗))))))
27		oveq1 7424	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑘 → (𝑖𝑥𝑚) = (𝑘𝑥𝑚))
28		oveq2 7425	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑙 → (𝑚𝑦𝑗) = (𝑚𝑦𝑙))
29	27, 28	oveqan12d 7436	. . . . . . . . . . 11 ⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑙) → ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)) = ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))
30	29	mpteq2dv 5203	. . . . . . . . . 10 ⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑙) → (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗))) = (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))
31	30	oveq2d 7433	. . . . . . . . 9 ⊢ ((𝑖 = 𝑘 ∧ 𝑗 = 𝑙) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))))
32	31	adantl 487	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ (𝑖 = 𝑘 ∧ 𝑗 = 𝑙)) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑖𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑗)))) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))))
33		simp2 1155	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑘 ∈ 𝑁)
34		simp3 1156	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑙 ∈ 𝑁)
35		ovexd 7452	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))) ∈ V)
36	26, 32, 33, 34, 35	ovmpod 7569	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑘(𝑥(.r‘𝐴)𝑦)𝑙) = (𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))))
37	36	fveq2d 6886	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)) = ((algSc‘𝑃)‘(𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))))
38		eqid 2762	. . . . . . 7 ⊢ (0g‘𝑅) = (0g‘𝑅)
39		ringcmn 20429	. . . . . . . . . 10 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
40	8, 39	syl 18	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ CMnd)
41	40	ad2antlr 740	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑅 ∈ CMnd)
42	41	3ad2ant1 1151	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑅 ∈ CMnd)
43		mat2pmatbas.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (Poly1‘𝑅)
44	43	ply1ring 22478	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
45	8, 44	syl 18	. . . . . . . . . 10 ⊢ (𝑅 ∈ CRing → 𝑃 ∈ Ring)
46		ringmnd 20388	. . . . . . . . . 10 ⊢ (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
47	45, 46	syl 18	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑃 ∈ Mnd)
48	47	ad2antlr 740	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Mnd)
49	48	3ad2ant1 1151	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑃 ∈ Mnd)
50	10	3ad2ant1 1151	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑁 ∈ Fin)
51		eqid 2762	. . . . . . . . . . . 12 ⊢ (algSc‘𝑃) = (algSc‘𝑃)
52		eqid 2762	. . . . . . . . . . . 12 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
53	45	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ Ring)
54	43	ply1lmod 22482	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
55	8, 54	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝑃 ∈ LMod)
56	55	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ LMod)
57	51, 52, 53, 56	asclghm 22103	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ ((Scalar‘𝑃) GrpHom 𝑃))
58	43	ply1sca 22483	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃))
59	58	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝑃))
60	59	oveq1d 7432	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 GrpHom 𝑃) = ((Scalar‘𝑃) GrpHom 𝑃))
61	57, 60	eleqtrrd 2865	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ (𝑅 GrpHom 𝑃))
62		ghmmhm 19359	. . . . . . . . . 10 ⊢ ((algSc‘𝑃) ∈ (𝑅 GrpHom 𝑃) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃))
63	61, 62	syl 18	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃))
64	63	adantr 486	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃))
65	64	3ad2ant1 1151	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃))
66	9	3ad2ant1 1151	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑅 ∈ Ring)
67	66	adantr 486	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑅 ∈ Ring)
68	33	adantr 486	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑘 ∈ 𝑁)
69		simpr 490	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑚 ∈ 𝑁)
70	14	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑥 ∈ (Base‘𝐴))
71	70	adantr 486	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑥 ∈ (Base‘𝐴))
72	71, 12	sylibr 237	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑥 ∈ 𝐵)
73	1, 6, 11, 68, 69, 72	matecld 22654	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑘𝑥𝑚) ∈ (Base‘𝑅))
74	34	adantr 486	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑙 ∈ 𝑁)
75	1	fveq2i 6885	. . . . . . . . . . . . . . . 16 ⊢ (Base‘𝐴) = (Base‘(𝑁 Mat 𝑅))
76	11, 75	eqtri 2785	. . . . . . . . . . . . . . 15 ⊢ 𝐵 = (Base‘(𝑁 Mat 𝑅))
77	76	eleq2i 2854	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
78	77	biimpi 219	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
79	78	ad2antll 742	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
80	79	3ad2ant1 1151	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
81	80	adantr 486	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
82	81, 77	sylibr 237	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ 𝐵)
83	1, 6, 11, 69, 74, 82	matecld 22654	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑚𝑦𝑙) ∈ (Base‘𝑅))
84	6, 7	ringcl 20395	. . . . . . . 8 ⊢ ((𝑅 ∈ Ring ∧ (𝑘𝑥𝑚) ∈ (Base‘𝑅) ∧ (𝑚𝑦𝑙) ∈ (Base‘𝑅)) → ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ (Base‘𝑅))
85	67, 73, 83, 84	syl3anc 1398	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ (Base‘𝑅))
86		eqid 2762	. . . . . . . 8 ⊢ (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) = (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))
87		ovexd 7452	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)) ∈ V)
88		fvexd 6897	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (0g‘𝑅) ∈ V)
89	86, 50, 87, 88	fsuppmptdm 9350	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) finSupp (0g‘𝑅))
90	6, 38, 42, 49, 50, 65, 85, 89	gsummptmhm 20073	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑃 Σg (𝑚 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) = ((algSc‘𝑃)‘(𝑅 Σg (𝑚 ∈ 𝑁 ↦ ((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))))
91	43	ply1assa 22430	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg)
92	91	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
93	51, 52	asclrhm 22111	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ AssAlg → (algSc‘𝑃) ∈ ((Scalar‘𝑃) RingHom 𝑃))
94	92, 93	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ ((Scalar‘𝑃) RingHom 𝑃))
95	59	oveq1d 7432	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
96	94, 95	eleqtrrd 2865	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃))
97	96	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃))
98	97	3ad2ant1 1151	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃))
99	98	adantr 486	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃))
100	20	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → 𝑦 ∈ (Base‘𝐴))
101	100	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ (Base‘𝐴))
102	101, 18	sylibr 237	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → 𝑦 ∈ 𝐵)
103	1, 6, 11, 69, 74, 102	matecld 22654	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → (𝑚𝑦𝑙) ∈ (Base‘𝑅))
104		eqid 2762	. . . . . . . . . 10 ⊢ (.r‘𝑃) = (.r‘𝑃)
105	6, 7, 104	rhmmul 20637	. . . . . . . . 9 ⊢ (((algSc‘𝑃) ∈ (𝑅 RingHom 𝑃) ∧ (𝑘𝑥𝑚) ∈ (Base‘𝑅) ∧ (𝑚𝑦𝑙) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) = (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))
106	99, 73, 103, 105	syl3anc 1398	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) ∧ 𝑚 ∈ 𝑁) → ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))) = (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))
107	106	mpteq2dva 5202	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑚 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙)))) = (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))
108	107	oveq2d 7433	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → (𝑃 Σg (𝑚 ∈ 𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r‘𝑅)(𝑚𝑦𝑙))))) = (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))))
109	37, 90, 108	3eqtr2d 2803	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙)) = (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))))
110	109	mpoeq3dva 7494	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙))) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))))
111		mat2pmatbas.c	. . . . 5 ⊢ 𝐶 = (𝑁 Mat 𝑃)
112		eqid 2762	. . . . 5 ⊢ (Base‘𝑃) = (Base‘𝑃)
113		eqid 2762	. . . . 5 ⊢ (.r‘𝐶) = (.r‘𝐶)
114	45	ad2antlr 740	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑃 ∈ Ring)
115		eqid 2762	. . . . 5 ⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))
116		eqid 2762	. . . . 5 ⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))
117	9	3ad2ant1 1151	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑅 ∈ Ring)
118		simp2 1155	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑖 ∈ 𝑁)
119		simp3 1156	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑗 ∈ 𝑁)
120		simp1rl 1257	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑥 ∈ 𝐵)
121	1, 6, 11, 118, 119, 120	matecld 22654	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝑥𝑗) ∈ (Base‘𝑅))
122	43, 51, 6, 112	ply1sclcl 22518	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑥𝑗) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘(𝑖𝑥𝑗)) ∈ (Base‘𝑃))
123	117, 121, 122	syl2anc 596	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑖𝑥𝑗)) ∈ (Base‘𝑃))
124		simp1rr 1258	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → 𝑦 ∈ 𝐵)
125	1, 6, 11, 118, 119, 124	matecld 22654	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑖𝑦𝑗) ∈ (Base‘𝑅))
126	43, 51, 6, 112	ply1sclcl 22518	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ (𝑖𝑦𝑗) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘(𝑖𝑦𝑗)) ∈ (Base‘𝑃))
127	117, 125, 126	syl2anc 596	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑖𝑦𝑗)) ∈ (Base‘𝑃))
128		oveq12 7426	. . . . . . 7 ⊢ ((𝑘 = 𝑖 ∧ 𝑚 = 𝑗) → (𝑘𝑥𝑚) = (𝑖𝑥𝑗))
129	128	fveq2d 6886	. . . . . 6 ⊢ ((𝑘 = 𝑖 ∧ 𝑚 = 𝑗) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) = ((algSc‘𝑃)‘(𝑖𝑥𝑗)))
130	129	adantl 487	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑘 = 𝑖 ∧ 𝑚 = 𝑗)) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) = ((algSc‘𝑃)‘(𝑖𝑥𝑗)))
131		oveq12 7426	. . . . . . 7 ⊢ ((𝑚 = 𝑖 ∧ 𝑙 = 𝑗) → (𝑚𝑦𝑙) = (𝑖𝑦𝑗))
132	131	fveq2d 6886	. . . . . 6 ⊢ ((𝑚 = 𝑖 ∧ 𝑙 = 𝑗) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗)))
133	132	adantl 487	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑚 = 𝑖 ∧ 𝑙 = 𝑗)) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗)))
134		fvexd 6897	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑘 ∈ 𝑁 ∧ 𝑚 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) ∈ V)
135		fvexd 6897	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑚 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) ∈ V)
136	111, 112, 113, 104, 114, 10, 115, 116, 123, 127, 130, 133, 134, 135	mpomatmul 22674	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r‘𝐶)(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ (𝑃 Σg (𝑚 ∈ 𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r‘𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))))
137	110, 136	eqtr4d 2800	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙))) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r‘𝐶)(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))))
138	1	matring 22671	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
139	8, 138	sylan2 605	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring)
140	139	anim1i 627	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐴 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
141		3anass 1111	. . . . . 6 ⊢ ((𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ↔ (𝐴 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
142	140, 141	sylibr 237	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))
143		eqid 2762	. . . . . 6 ⊢ (.r‘𝐴) = (.r‘𝐴)
144	11, 143	ringcl 20395	. . . . 5 ⊢ ((𝐴 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝐴)𝑦) ∈ 𝐵)
145	142, 144	syl 18	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐴)𝑦) ∈ 𝐵)
146		mat2pmatbas.t	. . . . 5 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
147	146, 1, 11, 43, 51	mat2pmatval 22955	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(.r‘𝐴)𝑦) ∈ 𝐵) → (𝑇‘(𝑥(.r‘𝐴)𝑦)) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙))))
148	10, 9, 145, 147	syl3anc 1398	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐴)𝑦)) = (𝑘 ∈ 𝑁, 𝑙 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r‘𝐴)𝑦)𝑙))))
149		simpl 488	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ 𝐵)
150	149	anim2i 629	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑥 ∈ 𝐵))
151		df-3an 1105	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑥 ∈ 𝐵))
152	150, 151	sylibr 237	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵))
153	146, 1, 11, 43, 51	mat2pmatval 22955	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥 ∈ 𝐵) → (𝑇‘𝑥) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))))
154	152, 153	syl 18	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑥) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))))
155		simpr 490	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
156	155	anim2i 629	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑦 ∈ 𝐵))
157		df-3an 1105	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑦 ∈ 𝐵))
158	156, 157	sylibr 237	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵))
159	146, 1, 11, 43, 51	mat2pmatval 22955	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦 ∈ 𝐵) → (𝑇‘𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))))
160	158, 159	syl 18	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘𝑦) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))))
161	154, 160	oveq12d 7435	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦)) = ((𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r‘𝐶)(𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))))
162	137, 148, 161	3eqtr4d 2807	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑇‘(𝑥(.r‘𝐴)𝑦)) = ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦)))
163	162	ralrimivva 3207	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐴)𝑦)) = ((𝑇‘𝑥)(.r‘𝐶)(𝑇‘𝑦)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3078  Vcvv 3453  ⟨cotp 4595   ↦ cmpt 5190   × cxp 5657  ‘cfv 6537  (class class class)co 7417   ∈ cmpo 7419   ↑_m cmap 8830  Fincfn 8956  Basecbs 17307  ._rcmulr 17349  Scalarcsca 17351  0_gc0g 17530   Σ_g cgsu 17531  Mndcmnd 18842   MndHom cmhm 18895   GrpHom cghm 19346  CMndccmn 19913  Ringcrg 20378  CRingccrg 20379   RingHom crh 20616  LModclmod 21050  AssAlgcasa 22071  algSccascl 22073  Poly₁cpl1 22408   maMul cmmul 22618   Mat cmat 22635   matToPolyMat cmat2pmat 22935

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-ot 4596  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-of 7682  df-ofr 7683  df-om 7867  df-1st 7990  df-2nd 7991  df-supp 8163  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-2o 8460  df-er 8700  df-map 8832  df-pm 8833  df-ixp 8909  df-en 8957  df-dom 8958  df-sdom 8959  df-fin 8960  df-fsupp 9336  df-sup 9416  df-oi 9486  df-card 9948  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-nn 12262  df-2 12331  df-3 12332  df-4 12333  df-5 12334  df-6 12335  df-7 12336  df-8 12337  df-9 12338  df-n0 12533  df-z 12620  df-dec 12741  df-uz 12892  df-fz 13566  df-fzo 13714  df-seq 14070  df-hash 14399  df-struct 17245  df-sets 17262  df-slot 17280  df-ndx 17292  df-base 17308  df-ress 17329  df-plusg 17361  df-mulr 17362  df-sca 17364  df-vsca 17365  df-ip 17366  df-tset 17367  df-ple 17368  df-ds 17370  df-hom 17372  df-cco 17373  df-0g 17532  df-gsum 17533  df-prds 17538  df-pws 17540  df-mre 17676  df-mrc 17677  df-acs 17679  df-mgm 18736  df-sgrp 18827  df-mnd 18843  df-mhm 18897  df-submnd 18898  df-grp 19066  df-minusg 19067  df-sbg 19068  df-mulg 19197  df-subg 19252  df-ghm 19347  df-cntz 19450  df-cmn 19915  df-abl 19916  df-mgp 20280  df-rng 20294  df-ur 20327  df-ring 20380  df-cring 20381  df-rhm 20619  df-subrng 20714  df-subrg 20738  df-lmod 21052  df-lss 21122  df-sra 21363  df-rgmod 21364  df-dsmm 21951  df-frlm 21966  df-assa 22074  df-ascl 22076  df-psr 22130  df-mpl 22132  df-opsr 22134  df-psr1 22411  df-ply1 22413  df-mamu 22619  df-mat 22636  df-mat2pmat 22938

This theorem is used by:  mat2pmatmhm  22964