MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mat2pmatmul Structured version   Visualization version   GIF version

Theorem mat2pmatmul 20829
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.
StepHypRef Expression
1 mat2pmatbas.a . . . . . . . . . . . . 13 𝐴 = (𝑁 Mat 𝑅)
2 eqid 2765 . . . . . . . . . . . . 13 (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)
31, 2matmulr 20534 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩) = (.r𝐴))
43eqcomd 2771 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (.r𝐴) = (𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩))
54oveqdr 6874 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(.r𝐴)𝑦) = (𝑥(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝑦))
6 eqid 2765 . . . . . . . . . . 11 (Base‘𝑅) = (Base‘𝑅)
7 eqid 2765 . . . . . . . . . . 11 (.r𝑅) = (.r𝑅)
8 crngring 18839 . . . . . . . . . . . 12 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
98ad2antlr 718 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑅 ∈ Ring)
10 simpll 783 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑁 ∈ Fin)
11 mat2pmatbas.b . . . . . . . . . . . . . . . 16 𝐵 = (Base‘𝐴)
1211eleq2i 2836 . . . . . . . . . . . . . . 15 (𝑥𝐵𝑥 ∈ (Base‘𝐴))
1312biimpi 207 . . . . . . . . . . . . . 14 (𝑥𝐵𝑥 ∈ (Base‘𝐴))
1413adantr 472 . . . . . . . . . . . . 13 ((𝑥𝐵𝑦𝐵) → 𝑥 ∈ (Base‘𝐴))
1514adantl 473 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑥 ∈ (Base‘𝐴))
161, 6matbas2 20517 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) = (Base‘𝐴))
1716adantr 472 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) = (Base‘𝐴))
1815, 17eleqtrrd 2847 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑥 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
1911eleq2i 2836 . . . . . . . . . . . . . 14 (𝑦𝐵𝑦 ∈ (Base‘𝐴))
2019biimpi 207 . . . . . . . . . . . . 13 (𝑦𝐵𝑦 ∈ (Base‘𝐴))
2120ad2antll 720 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 ∈ (Base‘𝐴))
2216eleq2d 2830 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) ↔ 𝑦 ∈ (Base‘𝐴)))
2322adantr 472 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)) ↔ 𝑦 ∈ (Base‘𝐴)))
2421, 23mpbird 248 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 ∈ ((Base‘𝑅) ↑𝑚 (𝑁 × 𝑁)))
252, 6, 7, 9, 10, 10, 10, 18, 24mamuval 20482 . . . . . . . . . 10 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(𝑅 maMul ⟨𝑁, 𝑁, 𝑁⟩)𝑦) = (𝑖𝑁, 𝑗𝑁 ↦ (𝑅 Σg (𝑚𝑁 ↦ ((𝑖𝑥𝑚)(.r𝑅)(𝑚𝑦𝑗))))))
265, 25eqtrd 2799 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(.r𝐴)𝑦) = (𝑖𝑁, 𝑗𝑁 ↦ (𝑅 Σg (𝑚𝑁 ↦ ((𝑖𝑥𝑚)(.r𝑅)(𝑚𝑦𝑗))))))
27263ad2ant1 1163 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (𝑥(.r𝐴)𝑦) = (𝑖𝑁, 𝑗𝑁 ↦ (𝑅 Σg (𝑚𝑁 ↦ ((𝑖𝑥𝑚)(.r𝑅)(𝑚𝑦𝑗))))))
28 oveq1 6853 . . . . . . . . . . . 12 (𝑖 = 𝑘 → (𝑖𝑥𝑚) = (𝑘𝑥𝑚))
29 oveq2 6854 . . . . . . . . . . . 12 (𝑗 = 𝑙 → (𝑚𝑦𝑗) = (𝑚𝑦𝑙))
3028, 29oveqan12d 6865 . . . . . . . . . . 11 ((𝑖 = 𝑘𝑗 = 𝑙) → ((𝑖𝑥𝑚)(.r𝑅)(𝑚𝑦𝑗)) = ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)))
3130mpteq2dv 4906 . . . . . . . . . 10 ((𝑖 = 𝑘𝑗 = 𝑙) → (𝑚𝑁 ↦ ((𝑖𝑥𝑚)(.r𝑅)(𝑚𝑦𝑗))) = (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙))))
3231oveq2d 6862 . . . . . . . . 9 ((𝑖 = 𝑘𝑗 = 𝑙) → (𝑅 Σg (𝑚𝑁 ↦ ((𝑖𝑥𝑚)(.r𝑅)(𝑚𝑦𝑗)))) = (𝑅 Σg (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)))))
3332adantl 473 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ (𝑖 = 𝑘𝑗 = 𝑙)) → (𝑅 Σg (𝑚𝑁 ↦ ((𝑖𝑥𝑚)(.r𝑅)(𝑚𝑦𝑗)))) = (𝑅 Σg (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)))))
34 simp2 1167 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → 𝑘𝑁)
35 simp3 1168 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → 𝑙𝑁)
36 ovexd 6880 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (𝑅 Σg (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)))) ∈ V)
3727, 33, 34, 35, 36ovmpt2d 6990 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (𝑘(𝑥(.r𝐴)𝑦)𝑙) = (𝑅 Σg (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)))))
3837fveq2d 6383 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → ((algSc‘𝑃)‘(𝑘(𝑥(.r𝐴)𝑦)𝑙)) = ((algSc‘𝑃)‘(𝑅 Σg (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙))))))
39 eqid 2765 . . . . . . 7 (0g𝑅) = (0g𝑅)
40 ringcmn 18862 . . . . . . . . . 10 (𝑅 ∈ Ring → 𝑅 ∈ CMnd)
418, 40syl 17 . . . . . . . . 9 (𝑅 ∈ CRing → 𝑅 ∈ CMnd)
4241ad2antlr 718 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑅 ∈ CMnd)
43423ad2ant1 1163 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → 𝑅 ∈ CMnd)
44 mat2pmatbas.p . . . . . . . . . . . 12 𝑃 = (Poly1𝑅)
4544ply1ring 19905 . . . . . . . . . . 11 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
468, 45syl 17 . . . . . . . . . 10 (𝑅 ∈ CRing → 𝑃 ∈ Ring)
47 ringmnd 18837 . . . . . . . . . 10 (𝑃 ∈ Ring → 𝑃 ∈ Mnd)
4846, 47syl 17 . . . . . . . . 9 (𝑅 ∈ CRing → 𝑃 ∈ Mnd)
4948ad2antlr 718 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑃 ∈ Mnd)
50493ad2ant1 1163 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → 𝑃 ∈ Mnd)
51103ad2ant1 1163 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → 𝑁 ∈ Fin)
52 eqid 2765 . . . . . . . . . . . 12 (algSc‘𝑃) = (algSc‘𝑃)
53 eqid 2765 . . . . . . . . . . . 12 (Scalar‘𝑃) = (Scalar‘𝑃)
5446adantl 473 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ Ring)
5544ply1lmod 19909 . . . . . . . . . . . . . 14 (𝑅 ∈ Ring → 𝑃 ∈ LMod)
568, 55syl 17 . . . . . . . . . . . . 13 (𝑅 ∈ CRing → 𝑃 ∈ LMod)
5756adantl 473 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ LMod)
5852, 53, 54, 57asclghm 19626 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ ((Scalar‘𝑃) GrpHom 𝑃))
5944ply1sca 19910 . . . . . . . . . . . . 13 (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃))
6059adantl 473 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 = (Scalar‘𝑃))
6160oveq1d 6861 . . . . . . . . . . 11 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 GrpHom 𝑃) = ((Scalar‘𝑃) GrpHom 𝑃))
6258, 61eleqtrrd 2847 . . . . . . . . . 10 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ (𝑅 GrpHom 𝑃))
63 ghmmhm 17948 . . . . . . . . . 10 ((algSc‘𝑃) ∈ (𝑅 GrpHom 𝑃) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃))
6462, 63syl 17 . . . . . . . . 9 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃))
6564adantr 472 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃))
66653ad2ant1 1163 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (algSc‘𝑃) ∈ (𝑅 MndHom 𝑃))
6793ad2ant1 1163 . . . . . . . . 9 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → 𝑅 ∈ Ring)
6867adantr 472 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑅 ∈ Ring)
6934adantr 472 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑘𝑁)
70 simpr 477 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑚𝑁)
71153ad2ant1 1163 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → 𝑥 ∈ (Base‘𝐴))
7271adantr 472 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑥 ∈ (Base‘𝐴))
7372, 12sylibr 225 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑥𝐵)
741, 6, 11, 69, 70, 73matecld 20522 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → (𝑘𝑥𝑚) ∈ (Base‘𝑅))
7535adantr 472 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑙𝑁)
761fveq2i 6382 . . . . . . . . . . . . . . . 16 (Base‘𝐴) = (Base‘(𝑁 Mat 𝑅))
7711, 76eqtri 2787 . . . . . . . . . . . . . . 15 𝐵 = (Base‘(𝑁 Mat 𝑅))
7877eleq2i 2836 . . . . . . . . . . . . . 14 (𝑦𝐵𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
7978biimpi 207 . . . . . . . . . . . . 13 (𝑦𝐵𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
8079ad2antll 720 . . . . . . . . . . . 12 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
81803ad2ant1 1163 . . . . . . . . . . 11 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
8281adantr 472 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑦 ∈ (Base‘(𝑁 Mat 𝑅)))
8382, 78sylibr 225 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑦𝐵)
841, 6, 11, 70, 75, 83matecld 20522 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → (𝑚𝑦𝑙) ∈ (Base‘𝑅))
856, 7ringcl 18842 . . . . . . . 8 ((𝑅 ∈ Ring ∧ (𝑘𝑥𝑚) ∈ (Base‘𝑅) ∧ (𝑚𝑦𝑙) ∈ (Base‘𝑅)) → ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)) ∈ (Base‘𝑅))
8668, 74, 84, 85syl3anc 1490 . . . . . . 7 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)) ∈ (Base‘𝑅))
87 eqid 2765 . . . . . . . 8 (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙))) = (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)))
88 ovexd 6880 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)) ∈ V)
89 fvexd 6394 . . . . . . . 8 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (0g𝑅) ∈ V)
9087, 51, 88, 89fsuppmptdm 8497 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙))) finSupp (0g𝑅))
916, 39, 43, 50, 51, 66, 86, 90gsummptmhm 18620 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (𝑃 Σg (𝑚𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙))))) = ((algSc‘𝑃)‘(𝑅 Σg (𝑚𝑁 ↦ ((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙))))))
9244ply1assa 19856 . . . . . . . . . . . . . . 15 (𝑅 ∈ CRing → 𝑃 ∈ AssAlg)
9392adantl 473 . . . . . . . . . . . . . 14 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑃 ∈ AssAlg)
9452, 53asclrhm 19630 . . . . . . . . . . . . . 14 (𝑃 ∈ AssAlg → (algSc‘𝑃) ∈ ((Scalar‘𝑃) RingHom 𝑃))
9593, 94syl 17 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ ((Scalar‘𝑃) RingHom 𝑃))
9660oveq1d 6861 . . . . . . . . . . . . 13 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑅 RingHom 𝑃) = ((Scalar‘𝑃) RingHom 𝑃))
9795, 96eleqtrrd 2847 . . . . . . . . . . . 12 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃))
9897adantr 472 . . . . . . . . . . 11 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃))
99983ad2ant1 1163 . . . . . . . . . 10 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃))
10099adantr 472 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → (algSc‘𝑃) ∈ (𝑅 RingHom 𝑃))
101213ad2ant1 1163 . . . . . . . . . . . 12 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → 𝑦 ∈ (Base‘𝐴))
102101adantr 472 . . . . . . . . . . 11 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑦 ∈ (Base‘𝐴))
103102, 19sylibr 225 . . . . . . . . . 10 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → 𝑦𝐵)
1041, 6, 11, 70, 75, 103matecld 20522 . . . . . . . . 9 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → (𝑚𝑦𝑙) ∈ (Base‘𝑅))
105 eqid 2765 . . . . . . . . . 10 (.r𝑃) = (.r𝑃)
1066, 7, 105rhmmul 19010 . . . . . . . . 9 (((algSc‘𝑃) ∈ (𝑅 RingHom 𝑃) ∧ (𝑘𝑥𝑚) ∈ (Base‘𝑅) ∧ (𝑚𝑦𝑙) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙))) = (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))
107100, 74, 104, 106syl3anc 1490 . . . . . . . 8 (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) ∧ 𝑚𝑁) → ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙))) = (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))
108107mpteq2dva 4905 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (𝑚𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙)))) = (𝑚𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))
109108oveq2d 6862 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → (𝑃 Σg (𝑚𝑁 ↦ ((algSc‘𝑃)‘((𝑘𝑥𝑚)(.r𝑅)(𝑚𝑦𝑙))))) = (𝑃 Σg (𝑚𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))))
11038, 91, 1093eqtr2d 2805 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑙𝑁) → ((algSc‘𝑃)‘(𝑘(𝑥(.r𝐴)𝑦)𝑙)) = (𝑃 Σg (𝑚𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙))))))
111110mpt2eq3dva 6921 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑘𝑁, 𝑙𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r𝐴)𝑦)𝑙))) = (𝑘𝑁, 𝑙𝑁 ↦ (𝑃 Σg (𝑚𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))))
112 mat2pmatbas.c . . . . 5 𝐶 = (𝑁 Mat 𝑃)
113 eqid 2765 . . . . 5 (Base‘𝑃) = (Base‘𝑃)
114 eqid 2765 . . . . 5 (.r𝐶) = (.r𝐶)
11546ad2antlr 718 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → 𝑃 ∈ Ring)
116 eqid 2765 . . . . 5 (𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))) = (𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))
117 eqid 2765 . . . . 5 (𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))) = (𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))
11893ad2ant1 1163 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑖𝑁𝑗𝑁) → 𝑅 ∈ Ring)
119 simp2 1167 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑖𝑁𝑗𝑁) → 𝑖𝑁)
120 simp3 1168 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑖𝑁𝑗𝑁) → 𝑗𝑁)
121 simp1rl 1319 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑖𝑁𝑗𝑁) → 𝑥𝐵)
1221, 6, 11, 119, 120, 121matecld 20522 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑖𝑁𝑗𝑁) → (𝑖𝑥𝑗) ∈ (Base‘𝑅))
12344, 52, 6, 113ply1sclcl 19943 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑖𝑥𝑗) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘(𝑖𝑥𝑗)) ∈ (Base‘𝑃))
124118, 122, 123syl2anc 579 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑖𝑁𝑗𝑁) → ((algSc‘𝑃)‘(𝑖𝑥𝑗)) ∈ (Base‘𝑃))
125 simp1rr 1320 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑖𝑁𝑗𝑁) → 𝑦𝐵)
1261, 6, 11, 119, 120, 125matecld 20522 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑖𝑁𝑗𝑁) → (𝑖𝑦𝑗) ∈ (Base‘𝑅))
12744, 52, 6, 113ply1sclcl 19943 . . . . . 6 ((𝑅 ∈ Ring ∧ (𝑖𝑦𝑗) ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘(𝑖𝑦𝑗)) ∈ (Base‘𝑃))
128118, 126, 127syl2anc 579 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑖𝑁𝑗𝑁) → ((algSc‘𝑃)‘(𝑖𝑦𝑗)) ∈ (Base‘𝑃))
129 oveq12 6855 . . . . . . 7 ((𝑘 = 𝑖𝑚 = 𝑗) → (𝑘𝑥𝑚) = (𝑖𝑥𝑗))
130129fveq2d 6383 . . . . . 6 ((𝑘 = 𝑖𝑚 = 𝑗) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) = ((algSc‘𝑃)‘(𝑖𝑥𝑗)))
131130adantl 473 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑘 = 𝑖𝑚 = 𝑗)) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) = ((algSc‘𝑃)‘(𝑖𝑥𝑗)))
132 oveq12 6855 . . . . . . 7 ((𝑚 = 𝑖𝑙 = 𝑗) → (𝑚𝑦𝑙) = (𝑖𝑦𝑗))
133132fveq2d 6383 . . . . . 6 ((𝑚 = 𝑖𝑙 = 𝑗) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗)))
134133adantl 473 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑚 = 𝑖𝑙 = 𝑗)) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) = ((algSc‘𝑃)‘(𝑖𝑦𝑗)))
135 fvexd 6394 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑘𝑁𝑚𝑁) → ((algSc‘𝑃)‘(𝑘𝑥𝑚)) ∈ V)
136 fvexd 6394 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) ∧ 𝑚𝑁𝑙𝑁) → ((algSc‘𝑃)‘(𝑚𝑦𝑙)) ∈ V)
137112, 113, 114, 105, 115, 10, 116, 117, 124, 128, 131, 134, 135, 136mpt2matmul 20543 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → ((𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r𝐶)(𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))) = (𝑘𝑁, 𝑙𝑁 ↦ (𝑃 Σg (𝑚𝑁 ↦ (((algSc‘𝑃)‘(𝑘𝑥𝑚))(.r𝑃)((algSc‘𝑃)‘(𝑚𝑦𝑙)))))))
138111, 137eqtr4d 2802 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑘𝑁, 𝑙𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r𝐴)𝑦)𝑙))) = ((𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r𝐶)(𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))))
1391matring 20539 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
1408, 139sylan2 586 . . . . . . 7 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring)
141140anim1i 608 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝐴 ∈ Ring ∧ (𝑥𝐵𝑦𝐵)))
142 3anass 1116 . . . . . 6 ((𝐴 ∈ Ring ∧ 𝑥𝐵𝑦𝐵) ↔ (𝐴 ∈ Ring ∧ (𝑥𝐵𝑦𝐵)))
143141, 142sylibr 225 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝐴 ∈ Ring ∧ 𝑥𝐵𝑦𝐵))
144 eqid 2765 . . . . . 6 (.r𝐴) = (.r𝐴)
14511, 144ringcl 18842 . . . . 5 ((𝐴 ∈ Ring ∧ 𝑥𝐵𝑦𝐵) → (𝑥(.r𝐴)𝑦) ∈ 𝐵)
146143, 145syl 17 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(.r𝐴)𝑦) ∈ 𝐵)
147 mat2pmatbas.t . . . . 5 𝑇 = (𝑁 matToPolyMat 𝑅)
148147, 1, 11, 44, 52mat2pmatval 20822 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(.r𝐴)𝑦) ∈ 𝐵) → (𝑇‘(𝑥(.r𝐴)𝑦)) = (𝑘𝑁, 𝑙𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r𝐴)𝑦)𝑙))))
14910, 9, 146, 148syl3anc 1490 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑇‘(𝑥(.r𝐴)𝑦)) = (𝑘𝑁, 𝑙𝑁 ↦ ((algSc‘𝑃)‘(𝑘(𝑥(.r𝐴)𝑦)𝑙))))
150 simpl 474 . . . . . . 7 ((𝑥𝐵𝑦𝐵) → 𝑥𝐵)
151150anim2i 610 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑥𝐵))
152 df-3an 1109 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑥𝐵))
153151, 152sylibr 225 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥𝐵))
154147, 1, 11, 44, 52mat2pmatval 20822 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑥𝐵) → (𝑇𝑥) = (𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))))
155153, 154syl 17 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑇𝑥) = (𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗))))
156 simpr 477 . . . . . . 7 ((𝑥𝐵𝑦𝐵) → 𝑦𝐵)
157156anim2i 610 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑦𝐵))
158 df-3an 1109 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑦𝐵))
159157, 158sylibr 225 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦𝐵))
160147, 1, 11, 44, 52mat2pmatval 20822 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑦𝐵) → (𝑇𝑦) = (𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))))
161159, 160syl 17 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑇𝑦) = (𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗))))
162155, 161oveq12d 6864 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → ((𝑇𝑥)(.r𝐶)(𝑇𝑦)) = ((𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑥𝑗)))(.r𝐶)(𝑖𝑁, 𝑗𝑁 ↦ ((algSc‘𝑃)‘(𝑖𝑦𝑗)))))
163138, 149, 1623eqtr4d 2809 . 2 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑥𝐵𝑦𝐵)) → (𝑇‘(𝑥(.r𝐴)𝑦)) = ((𝑇𝑥)(.r𝐶)(𝑇𝑦)))
164163ralrimivva 3118 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑥𝐵𝑦𝐵 (𝑇‘(𝑥(.r𝐴)𝑦)) = ((𝑇𝑥)(.r𝐶)(𝑇𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  Vcvv 3350  cotp 4344  cmpt 4890   × cxp 5277  cfv 6070  (class class class)co 6846  cmpt2 6848  𝑚 cmap 8064  Fincfn 8164  Basecbs 16144  .rcmulr 16229  Scalarcsca 16231  0gc0g 16380   Σg cgsu 16381  Mndcmnd 17574   MndHom cmhm 17613   GrpHom cghm 17935  CMndccmn 18473  Ringcrg 18828  CRingccrg 18829   RingHom crh 18995  LModclmod 19146  AssAlgcasa 19597  algSccascl 19599  Poly1cpl1 19834   maMul cmmul 20479   Mat cmat 20503   matToPolyMat cmat2pmat 20802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-inf2 8757  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-ot 4345  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-of 7099  df-ofr 7100  df-om 7268  df-1st 7370  df-2nd 7371  df-supp 7502  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-2o 7769  df-oadd 7772  df-er 7951  df-map 8066  df-pm 8067  df-ixp 8118  df-en 8165  df-dom 8166  df-sdom 8167  df-fin 8168  df-fsupp 8487  df-sup 8559  df-oi 8626  df-card 9020  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-nn 11279  df-2 11339  df-3 11340  df-4 11341  df-5 11342  df-6 11343  df-7 11344  df-8 11345  df-9 11346  df-n0 11543  df-z 11629  df-dec 11746  df-uz 11892  df-fz 12539  df-fzo 12679  df-seq 13014  df-hash 13327  df-struct 16146  df-ndx 16147  df-slot 16148  df-base 16150  df-sets 16151  df-ress 16152  df-plusg 16241  df-mulr 16242  df-sca 16244  df-vsca 16245  df-ip 16246  df-tset 16247  df-ple 16248  df-ds 16250  df-hom 16252  df-cco 16253  df-0g 16382  df-gsum 16383  df-prds 16388  df-pws 16390  df-mre 16526  df-mrc 16527  df-acs 16529  df-mgm 17522  df-sgrp 17564  df-mnd 17575  df-mhm 17615  df-submnd 17616  df-grp 17706  df-minusg 17707  df-sbg 17708  df-mulg 17822  df-subg 17869  df-ghm 17936  df-cntz 18027  df-cmn 18475  df-abl 18476  df-mgp 18771  df-ur 18783  df-ring 18830  df-cring 18831  df-rnghom 18998  df-subrg 19061  df-lmod 19148  df-lss 19216  df-sra 19460  df-rgmod 19461  df-assa 19600  df-ascl 19602  df-psr 19644  df-mpl 19646  df-opsr 19648  df-psr1 19837  df-ply1 19839  df-dsmm 20366  df-frlm 20381  df-mamu 20480  df-mat 20504  df-mat2pmat 20805
This theorem is referenced by:  mat2pmatmhm  20831
  Copyright terms: Public domain W3C validator