![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mp2pm2mplem5 | Structured version Visualization version GIF version |
Description: Lemma 5 for mp2pm2mp 20814. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.) |
Ref | Expression |
---|---|
mp2pm2mp.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
mp2pm2mp.q | ⊢ 𝑄 = (Poly1‘𝐴) |
mp2pm2mp.l | ⊢ 𝐿 = (Base‘𝑄) |
mp2pm2mp.m | ⊢ · = ( ·𝑠 ‘𝑃) |
mp2pm2mp.e | ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) |
mp2pm2mp.y | ⊢ 𝑌 = (var1‘𝑅) |
mp2pm2mp.i | ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) |
mp2pm2mplem2.p | ⊢ 𝑃 = (Poly1‘𝑅) |
mp2pm2mplem5.m | ⊢ ∗ = ( ·𝑠 ‘𝑄) |
mp2pm2mplem5.e | ⊢ ↑ = (.g‘(mulGrp‘𝑄)) |
mp2pm2mplem5.x | ⊢ 𝑋 = (var1‘𝐴) |
Ref | Expression |
---|---|
mp2pm2mplem5 | ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑘 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) finSupp (0g‘𝑄)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0ex 11486 | . . 3 ⊢ ℕ0 ∈ V | |
2 | 1 | a1i 11 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → ℕ0 ∈ V) |
3 | mp2pm2mp.a | . . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
4 | 3 | matring 20447 | . . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring) |
5 | mp2pm2mp.q | . . . . 5 ⊢ 𝑄 = (Poly1‘𝐴) | |
6 | 5 | ply1lmod 19820 | . . . 4 ⊢ (𝐴 ∈ Ring → 𝑄 ∈ LMod) |
7 | 4, 6 | syl 17 | . . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑄 ∈ LMod) |
8 | 7 | 3adant3 1127 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝑄 ∈ LMod) |
9 | 4 | 3adant3 1127 | . . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝐴 ∈ Ring) |
10 | 5 | ply1sca 19821 | . . 3 ⊢ (𝐴 ∈ Ring → 𝐴 = (Scalar‘𝑄)) |
11 | 9, 10 | syl 17 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → 𝐴 = (Scalar‘𝑄)) |
12 | mp2pm2mp.l | . 2 ⊢ 𝐿 = (Base‘𝑄) | |
13 | simpl2 1230 | . . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑘 ∈ ℕ0) → 𝑅 ∈ Ring) | |
14 | mp2pm2mplem2.p | . . . . 5 ⊢ 𝑃 = (Poly1‘𝑅) | |
15 | mp2pm2mp.m | . . . . 5 ⊢ · = ( ·𝑠 ‘𝑃) | |
16 | mp2pm2mp.e | . . . . 5 ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) | |
17 | mp2pm2mp.y | . . . . 5 ⊢ 𝑌 = (var1‘𝑅) | |
18 | mp2pm2mp.i | . . . . 5 ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) | |
19 | eqid 2756 | . . . . 5 ⊢ (𝑁 Mat 𝑃) = (𝑁 Mat 𝑃) | |
20 | eqid 2756 | . . . . 5 ⊢ (Base‘(𝑁 Mat 𝑃)) = (Base‘(𝑁 Mat 𝑃)) | |
21 | 3, 5, 12, 14, 15, 16, 17, 18, 19, 20 | mply1topmatcl 20808 | . . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃))) |
22 | 21 | adantr 472 | . . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑘 ∈ ℕ0) → (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃))) |
23 | simpr 479 | . . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0) | |
24 | eqid 2756 | . . . 4 ⊢ (Base‘𝐴) = (Base‘𝐴) | |
25 | 14, 19, 20, 3, 24 | decpmatcl 20770 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ (𝐼‘𝑂) ∈ (Base‘(𝑁 Mat 𝑃)) ∧ 𝑘 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝑘) ∈ (Base‘𝐴)) |
26 | 13, 22, 23, 25 | syl3anc 1477 | . 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑘 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝑘) ∈ (Base‘𝐴)) |
27 | mp2pm2mplem5.x | . . . 4 ⊢ 𝑋 = (var1‘𝐴) | |
28 | eqid 2756 | . . . 4 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄) | |
29 | mp2pm2mplem5.e | . . . 4 ⊢ ↑ = (.g‘(mulGrp‘𝑄)) | |
30 | 5, 27, 28, 29, 12 | ply1moncl 19839 | . . 3 ⊢ ((𝐴 ∈ Ring ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐿) |
31 | 9, 30 | sylan 489 | . 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑘 ∈ ℕ0) → (𝑘 ↑ 𝑋) ∈ 𝐿) |
32 | eqid 2756 | . 2 ⊢ (0g‘𝑄) = (0g‘𝑄) | |
33 | eqid 2756 | . 2 ⊢ (0g‘𝐴) = (0g‘𝐴) | |
34 | mp2pm2mplem5.m | . 2 ⊢ ∗ = ( ·𝑠 ‘𝑄) | |
35 | fveq2 6348 | . . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑙 → ((coe1‘𝑝)‘𝑘) = ((coe1‘𝑝)‘𝑙)) | |
36 | 35 | oveqd 6826 | . . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → (𝑖((coe1‘𝑝)‘𝑘)𝑗) = (𝑖((coe1‘𝑝)‘𝑙)𝑗)) |
37 | oveq1 6816 | . . . . . . . . . . . 12 ⊢ (𝑘 = 𝑙 → (𝑘𝐸𝑌) = (𝑙𝐸𝑌)) | |
38 | 36, 37 | oveq12d 6827 | . . . . . . . . . . 11 ⊢ (𝑘 = 𝑙 → ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)) = ((𝑖((coe1‘𝑝)‘𝑙)𝑗) · (𝑙𝐸𝑌))) |
39 | 38 | cbvmptv 4898 | . . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))) = (𝑙 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑙)𝑗) · (𝑙𝐸𝑌))) |
40 | 39 | oveq2i 6820 | . . . . . . . . 9 ⊢ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σg (𝑙 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑙)𝑗) · (𝑙𝐸𝑌)))) |
41 | 40 | a1i 11 | . . . . . . . 8 ⊢ ((𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁) → (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))) = (𝑃 Σg (𝑙 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑙)𝑗) · (𝑙𝐸𝑌))))) |
42 | 41 | mpt2eq3ia 6881 | . . . . . . 7 ⊢ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑙 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑙)𝑗) · (𝑙𝐸𝑌))))) |
43 | 42 | mpteq2i 4889 | . . . . . 6 ⊢ (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑙 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑙)𝑗) · (𝑙𝐸𝑌)))))) |
44 | 18, 43 | eqtri 2778 | . . . . 5 ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑙 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑙)𝑗) · (𝑙𝐸𝑌)))))) |
45 | 3, 5, 12, 15, 16, 17, 44, 14 | mp2pm2mplem4 20812 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝑘 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝑘) = ((coe1‘𝑂)‘𝑘)) |
46 | 45 | mpteq2dva 4892 | . . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑘 ∈ ℕ0 ↦ ((𝐼‘𝑂) decompPMat 𝑘)) = (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑂)‘𝑘))) |
47 | 5, 12, 33 | mptcoe1fsupp 19783 | . . . 4 ⊢ ((𝐴 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑂)‘𝑘)) finSupp (0g‘𝐴)) |
48 | 4, 47 | stoic3 1846 | . . 3 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑘 ∈ ℕ0 ↦ ((coe1‘𝑂)‘𝑘)) finSupp (0g‘𝐴)) |
49 | 46, 48 | eqbrtrd 4822 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑘 ∈ ℕ0 ↦ ((𝐼‘𝑂) decompPMat 𝑘)) finSupp (0g‘𝐴)) |
50 | 2, 8, 11, 12, 26, 31, 32, 33, 34, 49 | mptscmfsupp0 19126 | 1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑘 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) finSupp (0g‘𝑄)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 = wceq 1628 ∈ wcel 2135 Vcvv 3336 class class class wbr 4800 ↦ cmpt 4877 ‘cfv 6045 (class class class)co 6809 ↦ cmpt2 6811 Fincfn 8117 finSupp cfsupp 8436 ℕ0cn0 11480 Basecbs 16055 Scalarcsca 16142 ·𝑠 cvsca 16143 0gc0g 16298 Σg cgsu 16299 .gcmg 17737 mulGrpcmgp 18685 Ringcrg 18743 LModclmod 19061 var1cv1 19744 Poly1cpl1 19745 coe1cco1 19746 Mat cmat 20411 decompPMat cdecpmat 20765 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1867 ax-4 1882 ax-5 1984 ax-6 2050 ax-7 2086 ax-8 2137 ax-9 2144 ax-10 2164 ax-11 2179 ax-12 2192 ax-13 2387 ax-ext 2736 ax-rep 4919 ax-sep 4929 ax-nul 4937 ax-pow 4988 ax-pr 5051 ax-un 7110 ax-inf2 8707 ax-cnex 10180 ax-resscn 10181 ax-1cn 10182 ax-icn 10183 ax-addcl 10184 ax-addrcl 10185 ax-mulcl 10186 ax-mulrcl 10187 ax-mulcom 10188 ax-addass 10189 ax-mulass 10190 ax-distr 10191 ax-i2m1 10192 ax-1ne0 10193 ax-1rid 10194 ax-rnegex 10195 ax-rrecex 10196 ax-cnre 10197 ax-pre-lttri 10198 ax-pre-lttrn 10199 ax-pre-ltadd 10200 ax-pre-mulgt0 10201 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1631 df-fal 1634 df-ex 1850 df-nf 1855 df-sb 2043 df-eu 2607 df-mo 2608 df-clab 2743 df-cleq 2749 df-clel 2752 df-nfc 2887 df-ne 2929 df-nel 3032 df-ral 3051 df-rex 3052 df-reu 3053 df-rmo 3054 df-rab 3055 df-v 3338 df-sbc 3573 df-csb 3671 df-dif 3714 df-un 3716 df-in 3718 df-ss 3725 df-pss 3727 df-nul 4055 df-if 4227 df-pw 4300 df-sn 4318 df-pr 4320 df-tp 4322 df-op 4324 df-ot 4326 df-uni 4585 df-int 4624 df-iun 4670 df-iin 4671 df-br 4801 df-opab 4861 df-mpt 4878 df-tr 4901 df-id 5170 df-eprel 5175 df-po 5183 df-so 5184 df-fr 5221 df-se 5222 df-we 5223 df-xp 5268 df-rel 5269 df-cnv 5270 df-co 5271 df-dm 5272 df-rn 5273 df-res 5274 df-ima 5275 df-pred 5837 df-ord 5883 df-on 5884 df-lim 5885 df-suc 5886 df-iota 6008 df-fun 6047 df-fn 6048 df-f 6049 df-f1 6050 df-fo 6051 df-f1o 6052 df-fv 6053 df-isom 6054 df-riota 6770 df-ov 6812 df-oprab 6813 df-mpt2 6814 df-of 7058 df-ofr 7059 df-om 7227 df-1st 7329 df-2nd 7330 df-supp 7460 df-wrecs 7572 df-recs 7633 df-rdg 7671 df-1o 7725 df-2o 7726 df-oadd 7729 df-er 7907 df-map 8021 df-pm 8022 df-ixp 8071 df-en 8118 df-dom 8119 df-sdom 8120 df-fin 8121 df-fsupp 8437 df-sup 8509 df-oi 8576 df-card 8951 df-pnf 10264 df-mnf 10265 df-xr 10266 df-ltxr 10267 df-le 10268 df-sub 10456 df-neg 10457 df-nn 11209 df-2 11267 df-3 11268 df-4 11269 df-5 11270 df-6 11271 df-7 11272 df-8 11273 df-9 11274 df-n0 11481 df-z 11566 df-dec 11682 df-uz 11876 df-fz 12516 df-fzo 12656 df-seq 12992 df-hash 13308 df-struct 16057 df-ndx 16058 df-slot 16059 df-base 16061 df-sets 16062 df-ress 16063 df-plusg 16152 df-mulr 16153 df-sca 16155 df-vsca 16156 df-ip 16157 df-tset 16158 df-ple 16159 df-ds 16162 df-hom 16164 df-cco 16165 df-0g 16300 df-gsum 16301 df-prds 16306 df-pws 16308 df-mre 16444 df-mrc 16445 df-acs 16447 df-mgm 17439 df-sgrp 17481 df-mnd 17492 df-mhm 17532 df-submnd 17533 df-grp 17622 df-minusg 17623 df-sbg 17624 df-mulg 17738 df-subg 17788 df-ghm 17855 df-cntz 17946 df-cmn 18391 df-abl 18392 df-mgp 18686 df-ur 18698 df-ring 18745 df-subrg 18976 df-lmod 19063 df-lss 19131 df-sra 19370 df-rgmod 19371 df-psr 19554 df-mvr 19555 df-mpl 19556 df-opsr 19558 df-psr1 19748 df-vr1 19749 df-ply1 19750 df-coe1 19751 df-dsmm 20274 df-frlm 20289 df-mamu 20388 df-mat 20412 df-decpmat 20766 |
This theorem is referenced by: mp2pm2mp 20814 |
Copyright terms: Public domain | W3C validator |