| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cpmidg2sum | Structured version Visualization version GIF version | ||
| Description: Equality of two sums representing the identity matrix multiplied with the characteristic polynomial of a matrix. (Contributed by AV, 11-Nov-2019.) |
| Ref | Expression |
|---|---|
| cpmadugsum.a | ⊢ 𝐴 = (𝑁 Mat 𝑅) |
| cpmadugsum.b | ⊢ 𝐵 = (Base‘𝐴) |
| cpmadugsum.p | ⊢ 𝑃 = (Poly1‘𝑅) |
| cpmadugsum.y | ⊢ 𝑌 = (𝑁 Mat 𝑃) |
| cpmadugsum.t | ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) |
| cpmadugsum.x | ⊢ 𝑋 = (var1‘𝑅) |
| cpmadugsum.e | ⊢ ↑ = (.g‘(mulGrp‘𝑃)) |
| cpmadugsum.m | ⊢ · = ( ·𝑠 ‘𝑌) |
| cpmadugsum.r | ⊢ × = (.r‘𝑌) |
| cpmadugsum.1 | ⊢ 1 = (1r‘𝑌) |
| cpmadugsum.g | ⊢ + = (+g‘𝑌) |
| cpmadugsum.s | ⊢ − = (-g‘𝑌) |
| cpmadugsum.i | ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀)) |
| cpmadugsum.j | ⊢ 𝐽 = (𝑁 maAdju 𝑃) |
| cpmadugsum.0 | ⊢ 0 = (0g‘𝑌) |
| cpmadugsum.g2 | ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) |
| cpmidgsum2.c | ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) |
| cpmidgsum2.k | ⊢ 𝐾 = (𝐶‘𝑀) |
| cpmidg2sum.u | ⊢ 𝑈 = (algSc‘𝑃) |
| Ref | Expression |
|---|---|
| cpmidg2sum | ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · ((𝑈‘((coe1‘𝐾)‘𝑖)) · 1 )))) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cpmadugsum.a | . . . . . 6 ⊢ 𝐴 = (𝑁 Mat 𝑅) | |
| 2 | cpmadugsum.b | . . . . . 6 ⊢ 𝐵 = (Base‘𝐴) | |
| 3 | cpmadugsum.p | . . . . . 6 ⊢ 𝑃 = (Poly1‘𝑅) | |
| 4 | cpmadugsum.y | . . . . . 6 ⊢ 𝑌 = (𝑁 Mat 𝑃) | |
| 5 | cpmadugsum.x | . . . . . 6 ⊢ 𝑋 = (var1‘𝑅) | |
| 6 | cpmadugsum.e | . . . . . 6 ⊢ ↑ = (.g‘(mulGrp‘𝑃)) | |
| 7 | cpmadugsum.m | . . . . . 6 ⊢ · = ( ·𝑠 ‘𝑌) | |
| 8 | cpmadugsum.1 | . . . . . 6 ⊢ 1 = (1r‘𝑌) | |
| 9 | cpmidg2sum.u | . . . . . 6 ⊢ 𝑈 = (algSc‘𝑃) | |
| 10 | cpmidgsum2.c | . . . . . 6 ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) | |
| 11 | cpmidgsum2.k | . . . . . 6 ⊢ 𝐾 = (𝐶‘𝑀) | |
| 12 | eqid 2734 | . . . . . 6 ⊢ (𝐾 · 1 ) = (𝐾 · 1 ) | |
| 13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | cpmidgsum 22793 | . . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · ((𝑈‘((coe1‘𝐾)‘𝑖)) · 1 ))))) |
| 14 | 13 | eqcomd 2740 | . . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · ((𝑈‘((coe1‘𝐾)‘𝑖)) · 1 )))) = (𝐾 · 1 )) |
| 15 | 14 | ad3antrrr 730 | . . 3 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · ((𝑈‘((coe1‘𝐾)‘𝑖)) · 1 )))) = (𝐾 · 1 )) |
| 16 | simpr 484 | . . 3 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) → (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) | |
| 17 | 15, 16 | eqtrd 2769 | . 2 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ (𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · ((𝑈‘((coe1‘𝐾)‘𝑖)) · 1 )))) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) |
| 18 | cpmadugsum.t | . . 3 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) | |
| 19 | cpmadugsum.r | . . 3 ⊢ × = (.r‘𝑌) | |
| 20 | cpmadugsum.g | . . 3 ⊢ + = (+g‘𝑌) | |
| 21 | cpmadugsum.s | . . 3 ⊢ − = (-g‘𝑌) | |
| 22 | cpmadugsum.i | . . 3 ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀)) | |
| 23 | cpmadugsum.j | . . 3 ⊢ 𝐽 = (𝑁 maAdju 𝑃) | |
| 24 | cpmadugsum.0 | . . 3 ⊢ 0 = (0g‘𝑌) | |
| 25 | cpmadugsum.g2 | . . 3 ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) | |
| 26 | 1, 2, 3, 4, 18, 5, 6, 7, 19, 8, 20, 21, 22, 23, 24, 25, 10, 11, 12 | cpmidgsum2 22804 | . 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐾 · 1 ) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) |
| 27 | 17, 26 | reximddv2 3198 | 1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · ((𝑈‘((coe1‘𝐾)‘𝑖)) · 1 )))) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ∃wrex 3059 ifcif 4498 class class class wbr 5117 ↦ cmpt 5199 ‘cfv 6528 (class class class)co 7400 ↑m cmap 8835 Fincfn 8954 0cc0 11122 1c1 11123 + caddc 11125 < clt 11262 − cmin 11459 ℕcn 12233 ℕ0cn0 12494 ...cfz 13514 Basecbs 17215 +gcplusg 17258 .rcmulr 17259 ·𝑠 cvsca 17262 0gc0g 17440 Σg cgsu 17441 -gcsg 18905 .gcmg 19037 mulGrpcmgp 20087 1rcur 20128 CRingccrg 20181 algSccascl 21799 var1cv1 22098 Poly1cpl1 22099 coe1cco1 22100 Mat cmat 22332 maAdju cmadu 22557 matToPolyMat cmat2pmat 22629 CharPlyMat cchpmat 22751 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5247 ax-sep 5264 ax-nul 5274 ax-pow 5333 ax-pr 5400 ax-un 7724 ax-cnex 11178 ax-resscn 11179 ax-1cn 11180 ax-icn 11181 ax-addcl 11182 ax-addrcl 11183 ax-mulcl 11184 ax-mulrcl 11185 ax-mulcom 11186 ax-addass 11187 ax-mulass 11188 ax-distr 11189 ax-i2m1 11190 ax-1ne0 11191 ax-1rid 11192 ax-rnegex 11193 ax-rrecex 11194 ax-cnre 11195 ax-pre-lttri 11196 ax-pre-lttrn 11197 ax-pre-ltadd 11198 ax-pre-mulgt0 11199 ax-addf 11201 ax-mulf 11202 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-xor 1511 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3357 df-reu 3358 df-rab 3414 df-v 3459 df-sbc 3764 df-csb 3873 df-dif 3927 df-un 3929 df-in 3931 df-ss 3941 df-pss 3944 df-nul 4307 df-if 4499 df-pw 4575 df-sn 4600 df-pr 4602 df-tp 4604 df-op 4606 df-ot 4608 df-uni 4882 df-int 4921 df-iun 4967 df-iin 4968 df-br 5118 df-opab 5180 df-mpt 5200 df-tr 5228 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6288 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6530 df-fn 6531 df-f 6532 df-f1 6533 df-fo 6534 df-f1o 6535 df-fv 6536 df-isom 6537 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-of 7666 df-ofr 7667 df-om 7857 df-1st 7983 df-2nd 7984 df-supp 8155 df-tpos 8220 df-cur 8261 df-frecs 8275 df-wrecs 8306 df-recs 8380 df-rdg 8419 df-1o 8475 df-2o 8476 df-er 8714 df-map 8837 df-pm 8838 df-ixp 8907 df-en 8955 df-dom 8956 df-sdom 8957 df-fin 8958 df-fsupp 9369 df-sup 9449 df-oi 9517 df-card 9946 df-pnf 11264 df-mnf 11265 df-xr 11266 df-ltxr 11267 df-le 11268 df-sub 11461 df-neg 11462 df-div 11888 df-nn 12234 df-2 12296 df-3 12297 df-4 12298 df-5 12299 df-6 12300 df-7 12301 df-8 12302 df-9 12303 df-n0 12495 df-xnn0 12568 df-z 12582 df-dec 12702 df-uz 12846 df-rp 13002 df-fz 13515 df-fzo 13662 df-seq 14010 df-exp 14070 df-hash 14339 df-word 14522 df-lsw 14570 df-concat 14578 df-s1 14603 df-substr 14648 df-pfx 14678 df-splice 14757 df-reverse 14766 df-s2 14856 df-struct 17153 df-sets 17170 df-slot 17188 df-ndx 17200 df-base 17216 df-ress 17239 df-plusg 17271 df-mulr 17272 df-starv 17273 df-sca 17274 df-vsca 17275 df-ip 17276 df-tset 17277 df-ple 17278 df-ds 17280 df-unif 17281 df-hom 17282 df-cco 17283 df-0g 17442 df-gsum 17443 df-prds 17448 df-pws 17450 df-mre 17585 df-mrc 17586 df-acs 17588 df-mgm 18605 df-sgrp 18684 df-mnd 18700 df-mhm 18748 df-submnd 18749 df-efmnd 18834 df-grp 18906 df-minusg 18907 df-sbg 18908 df-mulg 19038 df-subg 19093 df-ghm 19183 df-gim 19229 df-cntz 19287 df-oppg 19316 df-symg 19338 df-pmtr 19410 df-psgn 19459 df-evpm 19460 df-cmn 19750 df-abl 19751 df-mgp 20088 df-rng 20100 df-ur 20129 df-srg 20134 df-ring 20182 df-cring 20183 df-oppr 20284 df-dvdsr 20304 df-unit 20305 df-invr 20335 df-dvr 20348 df-rhm 20419 df-subrng 20493 df-subrg 20517 df-drng 20678 df-lmod 20806 df-lss 20876 df-sra 21118 df-rgmod 21119 df-cnfld 21303 df-zring 21395 df-zrh 21451 df-dsmm 21679 df-frlm 21694 df-assa 21800 df-ascl 21802 df-psr 21856 df-mvr 21857 df-mpl 21858 df-opsr 21860 df-psr1 22102 df-vr1 22103 df-ply1 22104 df-coe1 22105 df-mamu 22316 df-mat 22333 df-mdet 22510 df-madu 22559 df-mat2pmat 22632 df-decpmat 22688 df-chpmat 22752 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |