Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > deg1pw | Structured version Visualization version GIF version | ||
| Description: Exact degree of a variable power over a nontrivial ring. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
| Ref | Expression |
|---|---|
| deg1pw.d | ⊢ 𝐷 = ( deg1 ‘𝑅) |
| deg1pw.p | ⊢ 𝑃 = (Poly1‘𝑅) |
| deg1pw.x | ⊢ 𝑋 = (var1‘𝑅) |
| deg1pw.n | ⊢ 𝑁 = (mulGrp‘𝑃) |
| deg1pw.e | ⊢ ↑ = (.g‘𝑁) |
| Ref | Expression |
|---|---|
| deg1pw | ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) = 𝐹) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | deg1pw.p | . . . . . . . 8 ⊢ 𝑃 = (Poly1‘𝑅) | |
| 2 | 1 | ply1sca 20977 | . . . . . . 7 ⊢ (𝑅 ∈ NzRing → 𝑅 = (Scalar‘𝑃)) |
| 3 | 2 | adantr 484 | . . . . . 6 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → 𝑅 = (Scalar‘𝑃)) |
| 4 | 3 | fveq2d 6662 | . . . . 5 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (1r‘𝑅) = (1r‘(Scalar‘𝑃))) |
| 5 | 4 | oveq1d 7165 | . . . 4 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → ((1r‘𝑅)( ·𝑠 ‘𝑃)(𝐹 ↑ 𝑋)) = ((1r‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝐹 ↑ 𝑋))) |
| 6 | nzrring 20102 | . . . . . . 7 ⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) | |
| 7 | 6 | adantr 484 | . . . . . 6 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → 𝑅 ∈ Ring) |
| 8 | 1 | ply1lmod 20976 | . . . . . 6 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
| 9 | 7, 8 | syl 17 | . . . . 5 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → 𝑃 ∈ LMod) |
| 10 | 1 | ply1ring 20972 | . . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 11 | deg1pw.n | . . . . . . . 8 ⊢ 𝑁 = (mulGrp‘𝑃) | |
| 12 | 11 | ringmgp 19371 | . . . . . . 7 ⊢ (𝑃 ∈ Ring → 𝑁 ∈ Mnd) |
| 13 | 7, 10, 12 | 3syl 18 | . . . . . 6 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → 𝑁 ∈ Mnd) |
| 14 | simpr 488 | . . . . . 6 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → 𝐹 ∈ ℕ0) | |
| 15 | deg1pw.x | . . . . . . . 8 ⊢ 𝑋 = (var1‘𝑅) | |
| 16 | eqid 2758 | . . . . . . . 8 ⊢ (Base‘𝑃) = (Base‘𝑃) | |
| 17 | 15, 1, 16 | vr1cl 20941 | . . . . . . 7 ⊢ (𝑅 ∈ Ring → 𝑋 ∈ (Base‘𝑃)) |
| 18 | 7, 17 | syl 17 | . . . . . 6 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → 𝑋 ∈ (Base‘𝑃)) |
| 19 | 11, 16 | mgpbas 19313 | . . . . . . 7 ⊢ (Base‘𝑃) = (Base‘𝑁) |
| 20 | deg1pw.e | . . . . . . 7 ⊢ ↑ = (.g‘𝑁) | |
| 21 | 19, 20 | mulgnn0cl 18311 | . . . . . 6 ⊢ ((𝑁 ∈ Mnd ∧ 𝐹 ∈ ℕ0 ∧ 𝑋 ∈ (Base‘𝑃)) → (𝐹 ↑ 𝑋) ∈ (Base‘𝑃)) |
| 22 | 13, 14, 18, 21 | syl3anc 1368 | . . . . 5 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (𝐹 ↑ 𝑋) ∈ (Base‘𝑃)) |
| 23 | eqid 2758 | . . . . . 6 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃) | |
| 24 | eqid 2758 | . . . . . 6 ⊢ ( ·𝑠 ‘𝑃) = ( ·𝑠 ‘𝑃) | |
| 25 | eqid 2758 | . . . . . 6 ⊢ (1r‘(Scalar‘𝑃)) = (1r‘(Scalar‘𝑃)) | |
| 26 | 16, 23, 24, 25 | lmodvs1 19730 | . . . . 5 ⊢ ((𝑃 ∈ LMod ∧ (𝐹 ↑ 𝑋) ∈ (Base‘𝑃)) → ((1r‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝐹 ↑ 𝑋)) = (𝐹 ↑ 𝑋)) |
| 27 | 9, 22, 26 | syl2anc 587 | . . . 4 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → ((1r‘(Scalar‘𝑃))( ·𝑠 ‘𝑃)(𝐹 ↑ 𝑋)) = (𝐹 ↑ 𝑋)) |
| 28 | 5, 27 | eqtrd 2793 | . . 3 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → ((1r‘𝑅)( ·𝑠 ‘𝑃)(𝐹 ↑ 𝑋)) = (𝐹 ↑ 𝑋)) |
| 29 | 28 | fveq2d 6662 | . 2 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (𝐷‘((1r‘𝑅)( ·𝑠 ‘𝑃)(𝐹 ↑ 𝑋))) = (𝐷‘(𝐹 ↑ 𝑋))) |
| 30 | eqid 2758 | . . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅) | |
| 31 | eqid 2758 | . . . . 5 ⊢ (1r‘𝑅) = (1r‘𝑅) | |
| 32 | 30, 31 | ringidcl 19389 | . . . 4 ⊢ (𝑅 ∈ Ring → (1r‘𝑅) ∈ (Base‘𝑅)) |
| 33 | 7, 32 | syl 17 | . . 3 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (1r‘𝑅) ∈ (Base‘𝑅)) |
| 34 | eqid 2758 | . . . . 5 ⊢ (0g‘𝑅) = (0g‘𝑅) | |
| 35 | 31, 34 | nzrnz 20101 | . . . 4 ⊢ (𝑅 ∈ NzRing → (1r‘𝑅) ≠ (0g‘𝑅)) |
| 36 | 35 | adantr 484 | . . 3 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (1r‘𝑅) ≠ (0g‘𝑅)) |
| 37 | deg1pw.d | . . . 4 ⊢ 𝐷 = ( deg1 ‘𝑅) | |
| 38 | 37, 30, 1, 15, 24, 11, 20, 34 | deg1tm 24818 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ ((1r‘𝑅) ∈ (Base‘𝑅) ∧ (1r‘𝑅) ≠ (0g‘𝑅)) ∧ 𝐹 ∈ ℕ0) → (𝐷‘((1r‘𝑅)( ·𝑠 ‘𝑃)(𝐹 ↑ 𝑋))) = 𝐹) |
| 39 | 7, 33, 36, 14, 38 | syl121anc 1372 | . 2 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (𝐷‘((1r‘𝑅)( ·𝑠 ‘𝑃)(𝐹 ↑ 𝑋))) = 𝐹) |
| 40 | 29, 39 | eqtr3d 2795 | 1 ⊢ ((𝑅 ∈ NzRing ∧ 𝐹 ∈ ℕ0) → (𝐷‘(𝐹 ↑ 𝑋)) = 𝐹) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ≠ wne 2951 ‘cfv 6335 (class class class)co 7150 ℕ0cn0 11934 Basecbs 16541 Scalarcsca 16626 ·𝑠 cvsca 16627 0gc0g 16771 Mndcmnd 17977 .gcmg 18291 mulGrpcmgp 19307 1rcur 19319 Ringcrg 19365 LModclmod 19702 NzRingcnzr 20098 var1cv1 20900 Poly1cpl1 20901 deg1 cdg1 24751 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5156 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652 ax-pre-sup 10653 ax-addf 10654 ax-mulf 10655 |
| This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-uni 4799 df-int 4839 df-iun 4885 df-iin 4886 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-se 5484 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-isom 6344 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-of 7405 df-ofr 7406 df-om 7580 df-1st 7693 df-2nd 7694 df-supp 7836 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-1o 8112 df-er 8299 df-map 8418 df-pm 8419 df-ixp 8480 df-en 8528 df-dom 8529 df-sdom 8530 df-fin 8531 df-fsupp 8867 df-sup 8939 df-oi 9007 df-card 9401 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-nn 11675 df-2 11737 df-3 11738 df-4 11739 df-5 11740 df-6 11741 df-7 11742 df-8 11743 df-9 11744 df-n0 11935 df-z 12021 df-dec 12138 df-uz 12283 df-fz 12940 df-fzo 13083 df-seq 13419 df-hash 13741 df-struct 16543 df-ndx 16544 df-slot 16545 df-base 16547 df-sets 16548 df-ress 16549 df-plusg 16636 df-mulr 16637 df-starv 16638 df-sca 16639 df-vsca 16640 df-tset 16642 df-ple 16643 df-ds 16645 df-unif 16646 df-0g 16773 df-gsum 16774 df-mre 16915 df-mrc 16916 df-acs 16918 df-mgm 17918 df-sgrp 17967 df-mnd 17978 df-mhm 18022 df-submnd 18023 df-grp 18172 df-minusg 18173 df-sbg 18174 df-mulg 18292 df-subg 18343 df-ghm 18423 df-cntz 18514 df-cmn 18975 df-abl 18976 df-mgp 19308 df-ur 19320 df-ring 19367 df-cring 19368 df-subrg 19601 df-lmod 19704 df-lss 19772 df-nzr 20099 df-cnfld 20167 df-psr 20671 df-mvr 20672 df-mpl 20673 df-opsr 20675 df-psr1 20904 df-vr1 20905 df-ply1 20906 df-coe1 20907 df-mdeg 24752 df-deg1 24753 |
| This theorem is referenced by: ply1remlem 24862 lgsqrlem4 26032 idomrootle 40512 |
| Copyright terms: Public domain | W3C validator |