pm2mpcl - Metamath Proof Explorer

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

Theorem pm2mpcl 22787

Description: The transformation of polynomial matrices into polynomials over matrices maps polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.)

**Hypotheses**
Ref	Expression
pm2mpval.p	⊢ 𝑃 = (Poly₁‘𝑅)
pm2mpval.c	⊢ 𝐶 = (𝑁 Mat 𝑃)
pm2mpval.b	⊢ 𝐵 = (Base‘𝐶)
pm2mpval.m	⊢ ∗ = ( ·_𝑠 ‘𝑄)
pm2mpval.e	⊢ ↑ = (._g‘(mulGrp‘𝑄))
pm2mpval.x	⊢ 𝑋 = (var₁‘𝐴)
pm2mpval.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
pm2mpval.q	⊢ 𝑄 = (Poly₁‘𝐴)
pm2mpval.t	⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)
pm2mpcl.l	⊢ 𝐿 = (Base‘𝑄)

**Assertion**
Ref	Expression
pm2mpcl	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ 𝐿)

Proof of Theorem pm2mpcl Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm2mpval.p	. . 3 ⊢ 𝑃 = (Poly₁‘𝑅)
2		pm2mpval.c	. . 3 ⊢ 𝐶 = (𝑁 Mat 𝑃)
3		pm2mpval.b	. . 3 ⊢ 𝐵 = (Base‘𝐶)
4		pm2mpval.m	. . 3 ⊢ ∗ = ( ·_𝑠 ‘𝑄)
5		pm2mpval.e	. . 3 ⊢ ↑ = (._g‘(mulGrp‘𝑄))
6		pm2mpval.x	. . 3 ⊢ 𝑋 = (var₁‘𝐴)
7		pm2mpval.a	. . 3 ⊢ 𝐴 = (𝑁 Mat 𝑅)
8		pm2mpval.q	. . 3 ⊢ 𝑄 = (Poly₁‘𝐴)
9		pm2mpval.t	. . 3 ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅)
10	1, 2, 3, 4, 5, 6, 7, 8, 9	pm2mpfval 22786	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))
11		pm2mpcl.l	. . 3 ⊢ 𝐿 = (Base‘𝑄)
12		eqid 2726	. . 3 ⊢ (0_g‘𝑄) = (0_g‘𝑄)
13	7	matring 22433	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
14	8	ply1ring 22233	. . . . 5 ⊢ (𝐴 ∈ Ring → 𝑄 ∈ Ring)
15		ringcmn 20257	. . . . 5 ⊢ (𝑄 ∈ Ring → 𝑄 ∈ CMnd)
16	13, 14, 15	3syl 18	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ CMnd)
17	16	3adant3 1129	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑄 ∈ CMnd)
18		nn0ex 12524	. . . 4 ⊢ ℕ₀ ∈ V
19	18	a1i 11	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ℕ₀ ∈ V)
20	13	3adant3 1129	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ Ring)
21	20	adantr 479	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝐴 ∈ Ring)
22		simpl2 1189	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑅 ∈ Ring)
23		simpl3 1190	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑀 ∈ 𝐵)
24		simpr 483	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → 𝑘 ∈ ℕ₀)
25		eqid 2726	. . . . . . 7 ⊢ (Base‘𝐴) = (Base‘𝐴)
26	1, 2, 3, 7, 25	decpmatcl 22757	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ∧ 𝑘 ∈ ℕ₀) → (𝑀 decompPMat 𝑘) ∈ (Base‘𝐴))
27	22, 23, 24, 26	syl3anc 1368	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (𝑀 decompPMat 𝑘) ∈ (Base‘𝐴))
28		eqid 2726	. . . . . 6 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
29	25, 8, 6, 4, 28, 5, 11	ply1tmcl 22259	. . . . 5 ⊢ ((𝐴 ∈ Ring ∧ (𝑀 decompPMat 𝑘) ∈ (Base‘𝐴) ∧ 𝑘 ∈ ℕ₀) → ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)) ∈ 𝐿)
30	21, 27, 24, 29	syl3anc 1368	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)) ∈ 𝐿)
31	30	fmpttd 7121	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))):ℕ₀⟶𝐿)
32	8	ply1lmod 22237	. . . . 5 ⊢ (𝐴 ∈ Ring → 𝑄 ∈ LMod)
33	20, 32	syl 17	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑄 ∈ LMod)
34		eqidd 2727	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝑄) = (Scalar‘𝑄))
35	8, 6, 28, 5, 11	ply1moncl 22258	. . . . 5 ⊢ ((𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ₀) → (𝑘 ↑ 𝑋) ∈ 𝐿)
36	20, 35	sylan 578	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑘 ∈ ℕ₀) → (𝑘 ↑ 𝑋) ∈ 𝐿)
37		eqid 2726	. . . 4 ⊢ (0_g‘(Scalar‘𝑄)) = (0_g‘(Scalar‘𝑄))
38		eqid 2726	. . . . . . 7 ⊢ (0_g‘𝐴) = (0_g‘𝐴)
39	1, 2, 3, 7, 38	decpmatfsupp 22759	. . . . . 6 ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ (𝑀 decompPMat 𝑘)) finSupp (0_g‘𝐴))
40	39	3adant1 1127	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ (𝑀 decompPMat 𝑘)) finSupp (0_g‘𝐴))
41	8	ply1sca 22238	. . . . . . . 8 ⊢ (𝐴 ∈ Ring → 𝐴 = (Scalar‘𝑄))
42	41	eqcomd 2732	. . . . . . 7 ⊢ (𝐴 ∈ Ring → (Scalar‘𝑄) = 𝐴)
43	20, 42	syl 17	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Scalar‘𝑄) = 𝐴)
44	43	fveq2d 6897	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (0_g‘(Scalar‘𝑄)) = (0_g‘𝐴))
45	40, 44	breqtrrd 5173	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ (𝑀 decompPMat 𝑘)) finSupp (0_g‘(Scalar‘𝑄)))
46	19, 33, 34, 11, 27, 36, 12, 37, 4, 45	mptscmfsupp0 20899	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ₀ ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) finSupp (0_g‘𝑄))
47	11, 12, 17, 19, 31, 46	gsumcl 19909	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑄 Σ_g (𝑘 ∈ ℕ₀ ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))) ∈ 𝐿)
48	10, 47	eqeltrd 2826	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ 𝐿)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 Vcvv 3462 class class class wbr 5145 ↦ cmpt 5228 ‘cfv 6546 (class class class)co 7416 Fincfn 8966 finSupp cfsupp 9398 ℕ₀cn0 12518 Basecbs 17208 Scalarcsca 17264 ·_𝑠 cvsca 17265 0_gc0g 17449 Σ_g cgsu 17450 ._gcmg 19057 CMndccmn 19774 mulGrpcmgp 20113 Ringcrg 20212 LModclmod 20832 var₁cv1 22161 Poly₁cpl1 22162 Mat cmat 22395 decompPMat cdecpmat 22752 pMatToMatPoly cpm2mp 22782

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5282 ax-sep 5296 ax-nul 5303 ax-pow 5361 ax-pr 5425 ax-un 7738 ax-cnex 11205 ax-resscn 11206 ax-1cn 11207 ax-icn 11208 ax-addcl 11209 ax-addrcl 11210 ax-mulcl 11211 ax-mulrcl 11212 ax-mulcom 11213 ax-addass 11214 ax-mulass 11215 ax-distr 11216 ax-i2m1 11217 ax-1ne0 11218 ax-1rid 11219 ax-rnegex 11220 ax-rrecex 11221 ax-cnre 11222 ax-pre-lttri 11223 ax-pre-lttrn 11224 ax-pre-ltadd 11225 ax-pre-mulgt0 11226

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3966 df-nul 4323 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-ot 4632 df-uni 4906 df-int 4947 df-iun 4995 df-iin 4996 df-br 5146 df-opab 5208 df-mpt 5229 df-tr 5263 df-id 5572 df-eprel 5578 df-po 5586 df-so 5587 df-fr 5629 df-se 5630 df-we 5631 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-res 5686 df-ima 5687 df-pred 6304 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6498 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-isom 6555 df-riota 7372 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7682 df-ofr 7683 df-om 7869 df-1st 7995 df-2nd 7996 df-supp 8167 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-er 8726 df-map 8849 df-pm 8850 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9399 df-sup 9478 df-oi 9546 df-card 9975 df-pnf 11291 df-mnf 11292 df-xr 11293 df-ltxr 11294 df-le 11295 df-sub 11487 df-neg 11488 df-nn 12259 df-2 12321 df-3 12322 df-4 12323 df-5 12324 df-6 12325 df-7 12326 df-8 12327 df-9 12328 df-n0 12519 df-z 12605 df-dec 12724 df-uz 12869 df-fz 13533 df-fzo 13676 df-seq 14016 df-hash 14343 df-struct 17144 df-sets 17161 df-slot 17179 df-ndx 17191 df-base 17209 df-ress 17238 df-plusg 17274 df-mulr 17275 df-sca 17277 df-vsca 17278 df-ip 17279 df-tset 17280 df-ple 17281 df-ds 17283 df-hom 17285 df-cco 17286 df-0g 17451 df-gsum 17452 df-prds 17457 df-pws 17459 df-mre 17594 df-mrc 17595 df-acs 17597 df-mgm 18628 df-sgrp 18707 df-mnd 18723 df-mhm 18768 df-submnd 18769 df-grp 18926 df-minusg 18927 df-sbg 18928 df-mulg 19058 df-subg 19113 df-ghm 19203 df-cntz 19307 df-cmn 19776 df-abl 19777 df-mgp 20114 df-rng 20132 df-ur 20161 df-ring 20214 df-subrng 20524 df-subrg 20549 df-lmod 20834 df-lss 20905 df-sra 21147 df-rgmod 21148 df-dsmm 21726 df-frlm 21741 df-psr 21902 df-mvr 21903 df-mpl 21904 df-opsr 21906 df-psr1 22165 df-vr1 22166 df-ply1 22167 df-coe1 22168 df-mamu 22379 df-mat 22396 df-decpmat 22753 df-pm2mp 22783

This theorem is referenced by: pm2mpf 22788 pm2mpf1 22789

W3C validator