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 21783

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 2738	. . 3 ⊢ (algSc‘𝑃) = (algSc‘𝑃)
6	1, 2, 3, 4, 5	mat2pmatval 21781	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑥𝑀𝑦))))
7		mat2pmatbas.c	. . 3 ⊢ 𝐶 = (𝑁 Mat 𝑃)
8		eqid 2738	. . 3 ⊢ (Base‘𝑃) = (Base‘𝑃)
9		eqid 2738	. . 3 ⊢ (Base‘𝐶) = (Base‘𝐶)
10		simp1 1134	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin)
11	4	fvexi 6770	. . . 4 ⊢ 𝑃 ∈ V
12	11	a1i 11	. . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ V)
13		eqid 2738	. . . . . 6 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
14	4	ply1ring 21329	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
15	14	3ad2ant2 1132	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ Ring)
16	15	3ad2ant1 1131	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑃 ∈ Ring)
17	4	ply1lmod 21333	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
18	17	3ad2ant2 1132	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑃 ∈ LMod)
19	18	3ad2ant1 1131	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑃 ∈ LMod)
20		eqid 2738	. . . . . 6 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
21	5, 13, 16, 19, 20, 8	asclf 20996	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (algSc‘𝑃):(Base‘(Scalar‘𝑃))⟶(Base‘𝑃))
22	4	ply1sca 21334	. . . . . . . . 9 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
23	22	fveq2d 6760	. . . . . . . 8 ⊢ (𝑅 ∈ Ring → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
24	23	3ad2ant2 1132	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
25	24	3ad2ant1 1131	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
26	25	feq2d 6570	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → ((algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃) ↔ (algSc‘𝑃):(Base‘(Scalar‘𝑃))⟶(Base‘𝑃)))
27	21, 26	mpbird 256	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (algSc‘𝑃):(Base‘𝑅)⟶(Base‘𝑃))
28		simp2 1135	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑥 ∈ 𝑁)
29		simp3 1136	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑦 ∈ 𝑁)
30	3	eleq2i 2830	. . . . . . . 8 ⊢ (𝑀 ∈ 𝐵 ↔ 𝑀 ∈ (Base‘𝐴))
31	30	biimpi 215	. . . . . . 7 ⊢ (𝑀 ∈ 𝐵 → 𝑀 ∈ (Base‘𝐴))
32	31	3ad2ant3 1133	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 ∈ (Base‘𝐴))
33	32	3ad2ant1 1131	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → 𝑀 ∈ (Base‘𝐴))
34		eqid 2738	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
35	2, 34	matecl 21482	. . . . 5 ⊢ ((𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁 ∧ 𝑀 ∈ (Base‘𝐴)) → (𝑥𝑀𝑦) ∈ (Base‘𝑅))
36	28, 29, 33, 35	syl3anc 1369	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → (𝑥𝑀𝑦) ∈ (Base‘𝑅))
37	27, 36	ffvelrnd 6944	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑥 ∈ 𝑁 ∧ 𝑦 ∈ 𝑁) → ((algSc‘𝑃)‘(𝑥𝑀𝑦)) ∈ (Base‘𝑃))
38	7, 8, 9, 10, 12, 37	matbas2d 21480	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑥 ∈ 𝑁, 𝑦 ∈ 𝑁 ↦ ((algSc‘𝑃)‘(𝑥𝑀𝑦))) ∈ (Base‘𝐶))
39	6, 38	eqeltrd 2839	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 Vcvv 3422 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ∈ cmpo 7257 Fincfn 8691 Basecbs 16840 Scalarcsca 16891 Ringcrg 19698 LModclmod 20038 algSccascl 20969 Poly₁cpl1 21258 Mat cmat 21464 matToPolyMat cmat2pmat 21761

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-ot 4567 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-ofr 7512 df-om 7688 df-1st 7804 df-2nd 7805 df-supp 7949 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-map 8575 df-pm 8576 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fsupp 9059 df-sup 9131 df-oi 9199 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-fz 13169 df-fzo 13312 df-seq 13650 df-hash 13973 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-sca 16904 df-vsca 16905 df-ip 16906 df-tset 16907 df-ple 16908 df-ds 16910 df-hom 16912 df-cco 16913 df-0g 17069 df-gsum 17070 df-prds 17075 df-pws 17077 df-mre 17212 df-mrc 17213 df-acs 17215 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-mhm 18345 df-submnd 18346 df-grp 18495 df-minusg 18496 df-sbg 18497 df-mulg 18616 df-subg 18667 df-ghm 18747 df-cntz 18838 df-cmn 19303 df-abl 19304 df-mgp 19636 df-ur 19653 df-ring 19700 df-subrg 19937 df-lmod 20040 df-lss 20109 df-sra 20349 df-rgmod 20350 df-dsmm 20849 df-frlm 20864 df-ascl 20972 df-psr 21022 df-mpl 21024 df-opsr 21026 df-psr1 21261 df-ply1 21263 df-mat 21465 df-mat2pmat 21764

This theorem is referenced by: mat2pmatbas0 21784 m2cpm 21798 m2pmfzmap 21804 monmatcollpw 21836 pmatcollpw 21838 chmatcl 21885 chmatval 21886 chpmat1dlem 21892 chpmat1d 21893 chpdmatlem1 21895 chpdmatlem2 21896 chpdmatlem3 21897 chfacfisf 21911 chfacfscmulgsum 21917 chfacfpmmulcl 21918 chfacfpmmul0 21919 chfacfpmmulgsum 21921 chfacfpmmulgsum2 21922 cayhamlem1 21923 cpmadugsumlemC 21932 cpmadugsumlemF 21933 cpmadugsumfi 21934 cpmidgsum2 21936

W3C validator