Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > cpmadumatpolylem1 | Structured version Visualization version GIF version | ||
| Description: Lemma 1 for cpmadumatpoly 23114. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 15-Dec-2019.) |
| Ref | Expression |
|---|---|
| cpmadumatpoly.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
| cpmadumatpoly.b | ⊢ 𝐵 = (Base‘𝐴) |
| cpmadumatpoly.p | ⊢ 𝑃 = (Poly1‘𝑅) |
| cpmadumatpoly.y | ⊢ 𝑌 = (𝑁 Mat 𝑃) |
| cpmadumatpoly.t | ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
| cpmadumatpoly.r | ⊢ × = (.r‘𝑌) |
| cpmadumatpoly.m0 | ⊢ − = (-g‘𝑌) |
| cpmadumatpoly.0 | ⊢ 0 = (0g‘𝑌) |
| cpmadumatpoly.g | ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
| cpmadumatpoly.s | ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) |
| cpmadumatpoly.m1 | ⊢ · = ( ·𝑠 ‘𝑌) |
| cpmadumatpoly.1 | ⊢ 1 = (1r‘𝑌) |
| cpmadumatpoly.z | ⊢ 𝑍 = (var1‘𝑅) |
| cpmadumatpoly.d | ⊢ 𝐷 = ((𝑍 · 1 ) − (𝑇‘𝑀)) |
| cpmadumatpoly.j | ⊢ 𝐽 = (𝑁 maAdju 𝑃) |
| cpmadumatpoly.w | ⊢ 𝑊 = (Base‘𝑌) |
| cpmadumatpoly.q | ⊢ 𝑄 = (Poly1‘𝐴) |
| cpmadumatpoly.x | ⊢ 𝑋 = (var1‘𝐴) |
| cpmadumatpoly.m2 | ⊢ ∗ = ( ·𝑠 ‘𝑄) |
| cpmadumatpoly.e | ⊢ ↑ = (.g‘(mulGrp‘𝑄)) |
| cpmadumatpoly.u | ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) |
| Ref | Expression |
|---|---|
| cpmadumatpolylem1 | ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simp1 1154 | . . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin) | |
| 2 | crngring 20390 | . . . . . . 7 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | |
| 3 | 2 | 3ad2ant2 1152 | . . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring) |
| 4 | 1, 3 | jca 521 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
| 5 | 4 | ad2antrr 739 | . . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring)) |
| 6 | cpmadumatpoly.a | . . . . 5 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
| 7 | cpmadumatpoly.b | . . . . 5 ⊢ 𝐵 = (Base‘𝐴) | |
| 8 | cpmadumatpoly.s | . . . . 5 ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) | |
| 9 | cpmadumatpoly.u | . . . . 5 ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) | |
| 10 | 6, 7, 8, 9 | cpm2mf 22983 | . . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑈:𝑆⟶𝐵) |
| 11 | 5, 10 | syl 18 | . . 3 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑈:𝑆⟶𝐵) |
| 12 | cpmadumatpoly.p | . . . . . 6 ⊢ 𝑃 = (Poly1‘𝑅) | |
| 13 | cpmadumatpoly.y | . . . . . 6 ⊢ 𝑌 = (𝑁 Mat 𝑃) | |
| 14 | cpmadumatpoly.r | . . . . . 6 ⊢ × = (.r‘𝑌) | |
| 15 | cpmadumatpoly.m0 | . . . . . 6 ⊢ − = (-g‘𝑌) | |
| 16 | cpmadumatpoly.0 | . . . . . 6 ⊢ 0 = (0g‘𝑌) | |
| 17 | cpmadumatpoly.t | . . . . . 6 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) | |
| 18 | cpmadumatpoly.g | . . . . . 6 ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) | |
| 19 | 6, 7, 12, 13, 14, 15, 16, 17, 18, 8 | chfacfisfcpmat 23086 | . . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶𝑆) |
| 20 | 2, 19 | syl3anl2 1440 | . . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶𝑆) |
| 21 | 20 | anassrs 473 | . . 3 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐺:ℕ0⟶𝑆) |
| 22 | fco 6731 | . . 3 ⊢ ((𝑈:𝑆⟶𝐵 ∧ 𝐺:ℕ0⟶𝑆) → (𝑈 ∘ 𝐺):ℕ0⟶𝐵) | |
| 23 | 11, 21, 22 | syl2anc 596 | . 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈 ∘ 𝐺):ℕ0⟶𝐵) |
| 24 | 7 | fvexi 6896 | . . . 4 ⊢ 𝐵 ∈ V |
| 25 | nn0ex 12538 | . . . 4 ⊢ ℕ0 ∈ V | |
| 26 | 24, 25 | pm3.2i 476 | . . 3 ⊢ (𝐵 ∈ V ∧ ℕ0 ∈ V) |
| 27 | elmapg 8842 | . . 3 ⊢ ((𝐵 ∈ V ∧ ℕ0 ∈ V) → ((𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0) ↔ (𝑈 ∘ 𝐺):ℕ0⟶𝐵)) | |
| 28 | 26, 27 | mp1i 14 | . 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → ((𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0) ↔ (𝑈 ∘ 𝐺):ℕ0⟶𝐵)) |
| 29 | 23, 28 | mpbird 260 | 1 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 Vcvv 3453 ifcif 4485 class class class wbr 5107 ↦ cmpt 5190 ∘ ccom 5663 ⟶wf 6533 ‘cfv 6537 (class class class)co 7417 ↑m cmap 8830 Fincfn 8956 0cc0 11128 1c1 11129 + caddc 11131 < clt 11271 − cmin 11469 ℕcn 12261 ℕ0cn0 12532 ...cfz 13565 Basecbs 17307 .rcmulr 17349 ·𝑠 cvsca 17352 0gc0g 17530 -gcsg 19065 .gcmg 19196 mulGrpcmgp 20279 1rcur 20326 Ringcrg 20378 CRingccrg 20379 var1cv1 22407 Poly1cpl1 22408 Mat cmat 22635 maAdju cmadu 22860 ConstPolyMat ccpmat 22934 matToPolyMat cmat2pmat 22935 cPolyMatToMat ccpmat2mat 22936 |
| 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 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 |
| 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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-ot 4596 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 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 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-ofr 7683 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-sup 9416 df-oi 9486 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12533 df-z 12620 df-dec 12741 df-uz 12892 df-fz 13566 df-fzo 13714 df-seq 14070 df-hash 14399 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-sca 17364 df-vsca 17365 df-ip 17366 df-tset 17367 df-ple 17368 df-ds 17370 df-hom 17372 df-cco 17373 df-0g 17532 df-gsum 17533 df-prds 17538 df-pws 17540 df-mre 17676 df-mrc 17677 df-acs 17679 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-mhm 18897 df-submnd 18898 df-grp 19066 df-minusg 19067 df-sbg 19068 df-mulg 19197 df-subg 19252 df-ghm 19347 df-cntz 19450 df-cmn 19915 df-abl 19916 df-mgp 20280 df-rng 20294 df-ur 20327 df-srg 20332 df-ring 20380 df-cring 20381 df-subrng 20714 df-subrg 20738 df-lmod 21052 df-lss 21122 df-sra 21363 df-rgmod 21364 df-dsmm 21951 df-frlm 21966 df-ascl 22076 df-psr 22130 df-mvr 22131 df-mpl 22132 df-opsr 22134 df-psr1 22411 df-vr1 22412 df-ply1 22413 df-coe1 22414 df-mamu 22619 df-mat 22636 df-cpmat 22937 df-mat2pmat 22938 df-cpmat2mat 22939 |
| This theorem is used by: cpmadumatpoly 23114 chcoeffeqlem 23116 |
| Copyright terms: Public domain | W3C validator |