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

Theorem chpidmat 20984
Description: The characteristic polynomial of the identity matrix. (Contributed by AV, 19-Aug-2019.)
Hypotheses
Ref Expression
chp0mat.c 𝐶 = (𝑁 CharPlyMat 𝑅)
chp0mat.p 𝑃 = (Poly1𝑅)
chp0mat.a 𝐴 = (𝑁 Mat 𝑅)
chp0mat.x 𝑋 = (var1𝑅)
chp0mat.g 𝐺 = (mulGrp‘𝑃)
chp0mat.m = (.g𝐺)
chpidmat.i 𝐼 = (1r𝐴)
chpidmat.s 𝑆 = (algSc‘𝑃)
chpidmat.1 1 = (1r𝑅)
chpidmat.m = (-g𝑃)
Assertion
Ref Expression
chpidmat ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐶𝐼) = ((♯‘𝑁) (𝑋 (𝑆1 ))))

Proof of Theorem chpidmat
Dummy variables 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 475 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑁 ∈ Fin)
2 simpr 478 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ CRing)
3 crngring 18878 . . . . 5 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
4 chp0mat.a . . . . . 6 𝐴 = (𝑁 Mat 𝑅)
54matring 20578 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
63, 5sylan2 587 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring)
7 eqid 2803 . . . . 5 (Base‘𝐴) = (Base‘𝐴)
8 chpidmat.i . . . . 5 𝐼 = (1r𝐴)
97, 8ringidcl 18888 . . . 4 (𝐴 ∈ Ring → 𝐼 ∈ (Base‘𝐴))
106, 9syl 17 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐼 ∈ (Base‘𝐴))
11 chpidmat.1 . . . . . . 7 1 = (1r𝑅)
12 eqid 2803 . . . . . . 7 (0g𝑅) = (0g𝑅)
131ad2antrr 718 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → 𝑁 ∈ Fin)
143adantl 474 . . . . . . . 8 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑅 ∈ Ring)
1514ad2antrr 718 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → 𝑅 ∈ Ring)
16 simplrl 796 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → 𝑖𝑁)
17 simplrr 797 . . . . . . 7 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → 𝑗𝑁)
184, 11, 12, 13, 15, 16, 17, 8mat1ov 20584 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → (𝑖𝐼𝑗) = if(𝑖 = 𝑗, 1 , (0g𝑅)))
19 ifnefalse 4293 . . . . . . 7 (𝑖𝑗 → if(𝑖 = 𝑗, 1 , (0g𝑅)) = (0g𝑅))
2019adantl 474 . . . . . 6 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → if(𝑖 = 𝑗, 1 , (0g𝑅)) = (0g𝑅))
2118, 20eqtrd 2837 . . . . 5 ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖𝑁𝑗𝑁)) ∧ 𝑖𝑗) → (𝑖𝐼𝑗) = (0g𝑅))
2221ex 402 . . . 4 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑖𝑁𝑗𝑁)) → (𝑖𝑗 → (𝑖𝐼𝑗) = (0g𝑅)))
2322ralrimivva 3156 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝐼𝑗) = (0g𝑅)))
24 chp0mat.c . . . 4 𝐶 = (𝑁 CharPlyMat 𝑅)
25 chp0mat.p . . . 4 𝑃 = (Poly1𝑅)
26 chpidmat.s . . . 4 𝑆 = (algSc‘𝑃)
27 chp0mat.x . . . 4 𝑋 = (var1𝑅)
28 chp0mat.g . . . 4 𝐺 = (mulGrp‘𝑃)
29 eqid 2803 . . . 4 (-g𝑃) = (-g𝑃)
3024, 25, 4, 26, 7, 27, 12, 28, 29chpdmat 20978 . . 3 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝐼 ∈ (Base‘𝐴)) ∧ ∀𝑖𝑁𝑗𝑁 (𝑖𝑗 → (𝑖𝐼𝑗) = (0g𝑅))) → (𝐶𝐼) = (𝐺 Σg (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆‘(𝑘𝐼𝑘))))))
311, 2, 10, 23, 30syl31anc 1493 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐶𝐼) = (𝐺 Σg (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆‘(𝑘𝐼𝑘))))))
321adantr 473 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘𝑁) → 𝑁 ∈ Fin)
3314adantr 473 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘𝑁) → 𝑅 ∈ Ring)
34 simpr 478 . . . . . . . . 9 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘𝑁) → 𝑘𝑁)
354, 11, 12, 32, 33, 34, 34, 8mat1ov 20584 . . . . . . . 8 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘𝑁) → (𝑘𝐼𝑘) = if(𝑘 = 𝑘, 1 , (0g𝑅)))
36 eqid 2803 . . . . . . . . 9 𝑘 = 𝑘
3736iftruei 4288 . . . . . . . 8 if(𝑘 = 𝑘, 1 , (0g𝑅)) = 1
3835, 37syl6eq 2853 . . . . . . 7 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘𝑁) → (𝑘𝐼𝑘) = 1 )
3938fveq2d 6419 . . . . . 6 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘𝑁) → (𝑆‘(𝑘𝐼𝑘)) = (𝑆1 ))
4039oveq2d 6898 . . . . 5 (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ 𝑘𝑁) → (𝑋(-g𝑃)(𝑆‘(𝑘𝐼𝑘))) = (𝑋(-g𝑃)(𝑆1 )))
4140mpteq2dva 4941 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆‘(𝑘𝐼𝑘)))) = (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆1 ))))
4241oveq2d 6898 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐺 Σg (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆‘(𝑘𝐼𝑘))))) = (𝐺 Σg (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆1 )))))
4325ply1crng 19894 . . . . . 6 (𝑅 ∈ CRing → 𝑃 ∈ CRing)
4428crngmgp 18875 . . . . . 6 (𝑃 ∈ CRing → 𝐺 ∈ CMnd)
45 cmnmnd 18527 . . . . . 6 (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
4643, 44, 453syl 18 . . . . 5 (𝑅 ∈ CRing → 𝐺 ∈ Mnd)
4746adantl 474 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐺 ∈ Mnd)
4825ply1ring 19944 . . . . . . . . . 10 (𝑅 ∈ Ring → 𝑃 ∈ Ring)
49 ringgrp 18872 . . . . . . . . . 10 (𝑃 ∈ Ring → 𝑃 ∈ Grp)
5048, 49syl 17 . . . . . . . . 9 (𝑅 ∈ Ring → 𝑃 ∈ Grp)
51 eqid 2803 . . . . . . . . . 10 (Base‘𝑃) = (Base‘𝑃)
5227, 25, 51vr1cl 19913 . . . . . . . . 9 (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
53 eqid 2803 . . . . . . . . . . 11 (1r𝑃) = (1r𝑃)
5425, 26, 11, 53ply1scl1 19988 . . . . . . . . . 10 (𝑅 ∈ Ring → (𝑆1 ) = (1r𝑃))
5551, 53ringidcl 18888 . . . . . . . . . . 11 (𝑃 ∈ Ring → (1r𝑃) ∈ (Base‘𝑃))
5648, 55syl 17 . . . . . . . . . 10 (𝑅 ∈ Ring → (1r𝑃) ∈ (Base‘𝑃))
5754, 56eqeltrd 2882 . . . . . . . . 9 (𝑅 ∈ Ring → (𝑆1 ) ∈ (Base‘𝑃))
5850, 52, 573jca 1159 . . . . . . . 8 (𝑅 ∈ Ring → (𝑃 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑃) ∧ (𝑆1 ) ∈ (Base‘𝑃)))
593, 58syl 17 . . . . . . 7 (𝑅 ∈ CRing → (𝑃 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑃) ∧ (𝑆1 ) ∈ (Base‘𝑃)))
6059adantl 474 . . . . . 6 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑃 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑃) ∧ (𝑆1 ) ∈ (Base‘𝑃)))
6151, 29grpsubcl 17815 . . . . . 6 ((𝑃 ∈ Grp ∧ 𝑋 ∈ (Base‘𝑃) ∧ (𝑆1 ) ∈ (Base‘𝑃)) → (𝑋(-g𝑃)(𝑆1 )) ∈ (Base‘𝑃))
6260, 61syl 17 . . . . 5 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑋(-g𝑃)(𝑆1 )) ∈ (Base‘𝑃))
6328, 51mgpbas 18815 . . . . 5 (Base‘𝑃) = (Base‘𝐺)
6462, 63syl6eleq 2892 . . . 4 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝑋(-g𝑃)(𝑆1 )) ∈ (Base‘𝐺))
65 eqid 2803 . . . . . 6 (Base‘𝐺) = (Base‘𝐺)
66 chp0mat.m . . . . . 6 = (.g𝐺)
6765, 66gsumconst 18653 . . . . 5 ((𝐺 ∈ Mnd ∧ 𝑁 ∈ Fin ∧ (𝑋(-g𝑃)(𝑆1 )) ∈ (Base‘𝐺)) → (𝐺 Σg (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆1 )))) = ((♯‘𝑁) (𝑋(-g𝑃)(𝑆1 ))))
68 chpidmat.m . . . . . . . 8 = (-g𝑃)
6968eqcomi 2812 . . . . . . 7 (-g𝑃) =
7069oveqi 6895 . . . . . 6 (𝑋(-g𝑃)(𝑆1 )) = (𝑋 (𝑆1 ))
7170oveq2i 6893 . . . . 5 ((♯‘𝑁) (𝑋(-g𝑃)(𝑆1 ))) = ((♯‘𝑁) (𝑋 (𝑆1 )))
7267, 71syl6eq 2853 . . . 4 ((𝐺 ∈ Mnd ∧ 𝑁 ∈ Fin ∧ (𝑋(-g𝑃)(𝑆1 )) ∈ (Base‘𝐺)) → (𝐺 Σg (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆1 )))) = ((♯‘𝑁) (𝑋 (𝑆1 ))))
7347, 1, 64, 72syl3anc 1491 . . 3 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐺 Σg (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆1 )))) = ((♯‘𝑁) (𝑋 (𝑆1 ))))
7442, 73eqtrd 2837 . 2 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐺 Σg (𝑘𝑁 ↦ (𝑋(-g𝑃)(𝑆‘(𝑘𝐼𝑘))))) = ((♯‘𝑁) (𝑋 (𝑆1 ))))
7531, 74eqtrd 2837 1 ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐶𝐼) = ((♯‘𝑁) (𝑋 (𝑆1 ))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108   = wceq 1653  wcel 2157  wne 2975  wral 3093  ifcif 4281  cmpt 4926  cfv 6105  (class class class)co 6882  Fincfn 8199  chash 13374  Basecbs 16188  0gc0g 16419   Σg cgsu 16420  Mndcmnd 17613  Grpcgrp 17742  -gcsg 17744  .gcmg 17860  CMndccmn 18512  mulGrpcmgp 18809  1rcur 18821  Ringcrg 18867  CRingccrg 18868  algSccascl 19638  var1cv1 19872  Poly1cpl1 19873   Mat cmat 20542   CharPlyMat cchpmat 20963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2379  ax-ext 2781  ax-rep 4968  ax-sep 4979  ax-nul 4987  ax-pow 5039  ax-pr 5101  ax-un 7187  ax-inf2 8792  ax-cnex 10284  ax-resscn 10285  ax-1cn 10286  ax-icn 10287  ax-addcl 10288  ax-addrcl 10289  ax-mulcl 10290  ax-mulrcl 10291  ax-mulcom 10292  ax-addass 10293  ax-mulass 10294  ax-distr 10295  ax-i2m1 10296  ax-1ne0 10297  ax-1rid 10298  ax-rnegex 10299  ax-rrecex 10300  ax-cnre 10301  ax-pre-lttri 10302  ax-pre-lttrn 10303  ax-pre-ltadd 10304  ax-pre-mulgt0 10305  ax-addf 10307  ax-mulf 10308
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-xor 1635  df-tru 1657  df-fal 1667  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2593  df-eu 2611  df-clab 2790  df-cleq 2796  df-clel 2799  df-nfc 2934  df-ne 2976  df-nel 3079  df-ral 3098  df-rex 3099  df-reu 3100  df-rmo 3101  df-rab 3102  df-v 3391  df-sbc 3638  df-csb 3733  df-dif 3776  df-un 3778  df-in 3780  df-ss 3787  df-pss 3789  df-nul 4120  df-if 4282  df-pw 4355  df-sn 4373  df-pr 4375  df-tp 4377  df-op 4379  df-ot 4381  df-uni 4633  df-int 4672  df-iun 4716  df-iin 4717  df-br 4848  df-opab 4910  df-mpt 4927  df-tr 4950  df-id 5224  df-eprel 5229  df-po 5237  df-so 5238  df-fr 5275  df-se 5276  df-we 5277  df-xp 5322  df-rel 5323  df-cnv 5324  df-co 5325  df-dm 5326  df-rn 5327  df-res 5328  df-ima 5329  df-pred 5902  df-ord 5948  df-on 5949  df-lim 5950  df-suc 5951  df-iota 6068  df-fun 6107  df-fn 6108  df-f 6109  df-f1 6110  df-fo 6111  df-f1o 6112  df-fv 6113  df-isom 6114  df-riota 6843  df-ov 6885  df-oprab 6886  df-mpt2 6887  df-of 7135  df-ofr 7136  df-om 7304  df-1st 7405  df-2nd 7406  df-supp 7537  df-tpos 7594  df-wrecs 7649  df-recs 7711  df-rdg 7749  df-1o 7803  df-2o 7804  df-oadd 7807  df-er 7986  df-map 8101  df-pm 8102  df-ixp 8153  df-en 8200  df-dom 8201  df-sdom 8202  df-fin 8203  df-fsupp 8522  df-sup 8594  df-oi 8661  df-card 9055  df-pnf 10369  df-mnf 10370  df-xr 10371  df-ltxr 10372  df-le 10373  df-sub 10562  df-neg 10563  df-div 10981  df-nn 11317  df-2 11380  df-3 11381  df-4 11382  df-5 11383  df-6 11384  df-7 11385  df-8 11386  df-9 11387  df-n0 11585  df-xnn0 11657  df-z 11671  df-dec 11788  df-uz 11935  df-rp 12079  df-fz 12585  df-fzo 12725  df-seq 13060  df-exp 13119  df-hash 13375  df-word 13539  df-lsw 13587  df-concat 13595  df-s1 13620  df-substr 13669  df-pfx 13718  df-splice 13825  df-reverse 13843  df-s2 13937  df-struct 16190  df-ndx 16191  df-slot 16192  df-base 16194  df-sets 16195  df-ress 16196  df-plusg 16284  df-mulr 16285  df-starv 16286  df-sca 16287  df-vsca 16288  df-ip 16289  df-tset 16290  df-ple 16291  df-ds 16293  df-unif 16294  df-hom 16295  df-cco 16296  df-0g 16421  df-gsum 16422  df-prds 16427  df-pws 16429  df-mre 16565  df-mrc 16566  df-acs 16568  df-mgm 17561  df-sgrp 17603  df-mnd 17614  df-mhm 17654  df-submnd 17655  df-grp 17745  df-minusg 17746  df-sbg 17747  df-mulg 17861  df-subg 17908  df-ghm 17975  df-gim 18018  df-cntz 18066  df-oppg 18092  df-symg 18114  df-pmtr 18178  df-psgn 18227  df-cmn 18514  df-abl 18515  df-mgp 18810  df-ur 18822  df-ring 18869  df-cring 18870  df-oppr 18943  df-dvdsr 18961  df-unit 18962  df-invr 18992  df-dvr 19003  df-rnghom 19037  df-drng 19071  df-subrg 19100  df-lmod 19187  df-lss 19255  df-sra 19499  df-rgmod 19500  df-ascl 19641  df-psr 19683  df-mvr 19684  df-mpl 19685  df-opsr 19687  df-psr1 19876  df-vr1 19877  df-ply1 19878  df-cnfld 20073  df-zring 20145  df-zrh 20178  df-dsmm 20405  df-frlm 20420  df-mamu 20519  df-mat 20543  df-mdet 20721  df-mat2pmat 20844  df-chpmat 20964
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator