mat2pmatbas - Metamath Proof Explorer

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

Theorem mat2pmatbas 23037

Description: The result of a matrix transformation is a polynomial matrix. (Contributed by AV, 1-Aug-2019.)

**Hypotheses**
Ref	Expression
mat2pmatbas.t	⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
mat2pmatbas.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
mat2pmatbas.b	⊢ 𝐵 = (Base‘𝐴)
mat2pmatbas.p	⊢ 𝑃 = (Poly₁‘𝑅)
mat2pmatbas.c	⊢ 𝐶 = (𝑁 Mat 𝑃)

**Assertion**
Ref	Expression
mat2pmatbas	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝐶))

Proof of Theorem mat2pmatbas Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	. . 3 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
2		mat2pmatbas.a	. . 3 ⊢ 𝐴 = (𝑁 Mat 𝑅)
3		mat2pmatbas.b	. . 3 ⊢ 𝐵 = (Base‘𝐴)
4		mat2pmatbas.p	. . 3 ⊢ 𝑃 = (Poly₁‘𝑅)
5		eqid 2761	. . 3 ⊢ (algSc‘𝑃) = (algSc‘𝑃)
6	1, 2, 3, 4, 5	mat2pmatval 23035	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑥𝑀𝑦))))
7		mat2pmatbas.c	. . 3 ⊢ 𝐶 = (𝑁 Mat 𝑃)
8		eqid 2761	. . 3 ⊢ (Base‘𝑃) = (Base‘𝑃)
9		eqid 2761	. . 3 ⊢ (Base‘𝐶) = (Base‘𝐶)
10		simp1 1154	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin)
11	4	fvexi 6897	. . . 4 ⊢ 𝑃 ∈ V
12	11	a1i 11	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ V)
13		eqid 2761	. . . . . 6 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
14	4	ply1ring 22558	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
15	14	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ Ring)
16	15	3ad2ant1 1151	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑃 ∈ Ring)
17	4	ply1lmod 22562	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
18	17	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ LMod)
19	18	3ad2ant1 1151	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑃 ∈ LMod)
20		eqid 2761	. . . . . 6 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
21	5, 13, 16, 19, 20, 8	asclf 22182	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (algSc‘𝑃):(Base‘(Scalar‘𝑃))⟶(Base‘𝑃))
22	4	ply1sca 22563	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
23	22	fveq2d 6887	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
24	23	3ad2ant2 1152	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
25	24	3ad2ant1 1151	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
26	25	feq2d 6691	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → ((algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃) ↔ (algSc‘𝑃):(Base‘(Scalar‘𝑃))⟶(Base‘𝑃)))
27	21, 26	mpbird 260	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃))
28		simp2 1155	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑥 ∈ 𝑁)
29		simp3 1156	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑦 ∈ 𝑁)
30	3	eleq2i 2853	. . . . . . . 8 ⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐴))
31	30	biimpi 219	. . . . . . 7 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (Base‘𝐴))
32	31	3ad2ant3 1153	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐴))
33	32	3ad2ant1 1151	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑀 ∈ (Base‘𝐴))
34		eqid 2761	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
35	2, 34	matecl 22733	. . . . 5 ⊢ ((𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝑥𝑀𝑦) ∈ (Base‘𝑅))
36	28, 29, 33, 35	syl3anc 1398	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (𝑥𝑀𝑦) ∈ (Base‘𝑅))
37	27, 36	ffvelcdmd 7083	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑥𝑀𝑦)) ∈ (Base‘𝑃))
38	7, 8, 9, 10, 12, 37	matbas2d 22731	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑥𝑀𝑦))) ∈ (Base‘𝐶))
39	6, 38	eqeltrd 2861	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 Vcvv 3451 ⟶wf 6533 ‘cfv 6537 (class class class)co 7418 ∈ cmpo 7420 Fincfn 8966 Basecbs 17380 Scalarcsca 17424 Ringcrg 20452 LModclmod 21128 algSccascl 22153 Poly₁cpl1 22488 Mat cmat 22715 matToPolyMat cmat2pmat 23015

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 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-ot 4593 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 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 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-ofr 7692 df-om 7876 df-1st 7999 df-2nd 8000 df-supp 8171 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9347 df-sup 9427 df-oi 9497 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-z 12687 df-dec 12808 df-uz 12959 df-fz 13633 df-fzo 13782 df-seq 14138 df-hash 14468 df-struct 17318 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-sca 17437 df-vsca 17438 df-ip 17439 df-tset 17440 df-ple 17441 df-ds 17443 df-hom 17445 df-cco 17446 df-0g 17605 df-gsum 17606 df-prds 17611 df-pws 17613 df-mre 17749 df-mrc 17750 df-acs 17752 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-mhm 18971 df-submnd 18972 df-grp 19140 df-minusg 19141 df-sbg 19142 df-mulg 19271 df-subg 19326 df-ghm 19421 df-cntz 19524 df-cmn 19989 df-abl 19990 df-mgp 20354 df-rng 20368 df-ur 20401 df-ring 20454 df-subrng 20791 df-subrg 20815 df-lmod 21130 df-lss 21200 df-sra 21441 df-rgmod 21442 df-dsmm 22031 df-frlm 22046 df-ascl 22156 df-psr 22210 df-mpl 22212 df-opsr 22214 df-psr1 22491 df-ply1 22493 df-mat 22716 df-mat2pmat 23018

This theorem is used by: mat2pmatbas0 23038 m2cpm 23052 m2pmfzmap 23058 monmatcollpw 23090 pmatcollpw 23092 chmatcl 23139 chmatval 23140 chpmat1dlem 23146 chpmat1d 23147 chpdmatlem1 23149 chpdmatlem2 23150 chpdmatlem3 23151 chfacfisf 23165 chfacfscmulgsum 23171 chfacfpmmulcl 23172 chfacfpmmul0 23173 chfacfpmmulgsum 23175 chfacfpmmulgsum2 23176 cayhamlem1 23177 cpmadugsumlemC 23186 cpmadugsumlemF 23187 cpmadugsumfi 23188 cpmidgsum2 23190

W3C validator