Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > coe1mul4 | Structured version Visualization version GIF version |
Description: Value of the "leading" coefficient of a product of two nonzero polynomials. This will fail to actually be the leading coefficient only if it is zero (requiring the basic ring to contain zero divisors). (Contributed by Stefan O'Rear, 25-Mar-2015.) |
Ref | Expression |
---|---|
coe1mul3.s | ⊢ 𝑌 = (Poly1‘𝑅) |
coe1mul3.t | ⊢ ∙ = (.r‘𝑌) |
coe1mul3.u | ⊢ · = (.r‘𝑅) |
coe1mul3.b | ⊢ 𝐵 = (Base‘𝑌) |
coe1mul3.d | ⊢ 𝐷 = ( deg1 ‘𝑅) |
coe1mul4.z | ⊢ 0 = (0g‘𝑌) |
coe1mul4.r | ⊢ (𝜑 → 𝑅 ∈ Ring) |
coe1mul4.f1 | ⊢ (𝜑 → 𝐹 ∈ 𝐵) |
coe1mul4.f2 | ⊢ (𝜑 → 𝐹 ≠ 0 ) |
coe1mul4.g1 | ⊢ (𝜑 → 𝐺 ∈ 𝐵) |
coe1mul4.g2 | ⊢ (𝜑 → 𝐺 ≠ 0 ) |
Ref | Expression |
---|---|
coe1mul4 | ⊢ (𝜑 → ((coe1‘(𝐹 ∙ 𝐺))‘((𝐷‘𝐹) + (𝐷‘𝐺))) = (((coe1‘𝐹)‘(𝐷‘𝐹)) · ((coe1‘𝐺)‘(𝐷‘𝐺)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coe1mul3.s | . 2 ⊢ 𝑌 = (Poly1‘𝑅) | |
2 | coe1mul3.t | . 2 ⊢ ∙ = (.r‘𝑌) | |
3 | coe1mul3.u | . 2 ⊢ · = (.r‘𝑅) | |
4 | coe1mul3.b | . 2 ⊢ 𝐵 = (Base‘𝑌) | |
5 | coe1mul3.d | . 2 ⊢ 𝐷 = ( deg1 ‘𝑅) | |
6 | coe1mul4.r | . 2 ⊢ (𝜑 → 𝑅 ∈ Ring) | |
7 | coe1mul4.f1 | . 2 ⊢ (𝜑 → 𝐹 ∈ 𝐵) | |
8 | coe1mul4.f2 | . . 3 ⊢ (𝜑 → 𝐹 ≠ 0 ) | |
9 | coe1mul4.z | . . . 4 ⊢ 0 = (0g‘𝑌) | |
10 | 5, 1, 9, 4 | deg1nn0cl 25241 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → (𝐷‘𝐹) ∈ ℕ0) |
11 | 6, 7, 8, 10 | syl3anc 1370 | . 2 ⊢ (𝜑 → (𝐷‘𝐹) ∈ ℕ0) |
12 | 11 | nn0red 12282 | . . 3 ⊢ (𝜑 → (𝐷‘𝐹) ∈ ℝ) |
13 | 12 | leidd 11529 | . 2 ⊢ (𝜑 → (𝐷‘𝐹) ≤ (𝐷‘𝐹)) |
14 | coe1mul4.g1 | . 2 ⊢ (𝜑 → 𝐺 ∈ 𝐵) | |
15 | coe1mul4.g2 | . . 3 ⊢ (𝜑 → 𝐺 ≠ 0 ) | |
16 | 5, 1, 9, 4 | deg1nn0cl 25241 | . . 3 ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵 ∧ 𝐺 ≠ 0 ) → (𝐷‘𝐺) ∈ ℕ0) |
17 | 6, 14, 15, 16 | syl3anc 1370 | . 2 ⊢ (𝜑 → (𝐷‘𝐺) ∈ ℕ0) |
18 | 17 | nn0red 12282 | . . 3 ⊢ (𝜑 → (𝐷‘𝐺) ∈ ℝ) |
19 | 18 | leidd 11529 | . 2 ⊢ (𝜑 → (𝐷‘𝐺) ≤ (𝐷‘𝐺)) |
20 | 1, 2, 3, 4, 5, 6, 7, 11, 13, 14, 17, 19 | coe1mul3 25252 | 1 ⊢ (𝜑 → ((coe1‘(𝐹 ∙ 𝐺))‘((𝐷‘𝐹) + (𝐷‘𝐺))) = (((coe1‘𝐹)‘(𝐷‘𝐹)) · ((coe1‘𝐺)‘(𝐷‘𝐺)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ‘cfv 6427 (class class class)co 7268 + caddc 10862 ℕ0cn0 12221 Basecbs 16900 .rcmulr 16951 0gc0g 17138 Ringcrg 19771 Poly1cpl1 21336 coe1cco1 21337 deg1 cdg1 25204 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5222 ax-nul 5229 ax-pow 5287 ax-pr 5351 ax-un 7579 ax-cnex 10915 ax-resscn 10916 ax-1cn 10917 ax-icn 10918 ax-addcl 10919 ax-addrcl 10920 ax-mulcl 10921 ax-mulrcl 10922 ax-mulcom 10923 ax-addass 10924 ax-mulass 10925 ax-distr 10926 ax-i2m1 10927 ax-1ne0 10928 ax-1rid 10929 ax-rnegex 10930 ax-rrecex 10931 ax-cnre 10932 ax-pre-lttri 10933 ax-pre-lttrn 10934 ax-pre-ltadd 10935 ax-pre-mulgt0 10936 ax-pre-sup 10937 ax-addf 10938 ax-mulf 10939 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3432 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-int 4881 df-iun 4927 df-iin 4928 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5485 df-eprel 5491 df-po 5499 df-so 5500 df-fr 5540 df-se 5541 df-we 5542 df-xp 5591 df-rel 5592 df-cnv 5593 df-co 5594 df-dm 5595 df-rn 5596 df-res 5597 df-ima 5598 df-pred 6196 df-ord 6263 df-on 6264 df-lim 6265 df-suc 6266 df-iota 6385 df-fun 6429 df-fn 6430 df-f 6431 df-f1 6432 df-fo 6433 df-f1o 6434 df-fv 6435 df-isom 6436 df-riota 7225 df-ov 7271 df-oprab 7272 df-mpo 7273 df-of 7524 df-ofr 7525 df-om 7704 df-1st 7821 df-2nd 7822 df-supp 7966 df-frecs 8085 df-wrecs 8116 df-recs 8190 df-rdg 8229 df-1o 8285 df-er 8486 df-map 8605 df-pm 8606 df-ixp 8674 df-en 8722 df-dom 8723 df-sdom 8724 df-fin 8725 df-fsupp 9117 df-sup 9189 df-oi 9257 df-card 9685 df-pnf 10999 df-mnf 11000 df-xr 11001 df-ltxr 11002 df-le 11003 df-sub 11195 df-neg 11196 df-nn 11962 df-2 12024 df-3 12025 df-4 12026 df-5 12027 df-6 12028 df-7 12029 df-8 12030 df-9 12031 df-n0 12222 df-z 12308 df-dec 12426 df-uz 12571 df-fz 13228 df-fzo 13371 df-seq 13710 df-hash 14033 df-struct 16836 df-sets 16853 df-slot 16871 df-ndx 16883 df-base 16901 df-ress 16930 df-plusg 16963 df-mulr 16964 df-starv 16965 df-sca 16966 df-vsca 16967 df-tset 16969 df-ple 16970 df-ds 16972 df-unif 16973 df-0g 17140 df-gsum 17141 df-mre 17283 df-mrc 17284 df-acs 17286 df-mgm 18314 df-sgrp 18363 df-mnd 18374 df-mhm 18418 df-submnd 18419 df-grp 18568 df-minusg 18569 df-mulg 18689 df-subg 18740 df-ghm 18820 df-cntz 18911 df-cmn 19376 df-abl 19377 df-mgp 19709 df-ur 19726 df-ring 19773 df-cring 19774 df-cnfld 20586 df-psr 21100 df-mpl 21102 df-opsr 21104 df-psr1 21339 df-ply1 21341 df-coe1 21342 df-mdeg 25205 df-deg1 25206 |
This theorem is referenced by: deg1mul2 25267 mon1psubm 41017 |
Copyright terms: Public domain | W3C validator |