evlsexpval - Metamath Proof Explorer

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

Theorem evlsexpval 22437

Description: Polynomial evaluation builder for exponentiation. (Contributed by SN, 27-Jul-2024.)

**Hypotheses**
Ref	Expression
evlsaddval.q	⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
evlsaddval.p	⊢ 𝑃 = (𝐼 mPoly 𝑈)
evlsaddval.u	⊢ 𝑈 = (𝑆 ↾_s 𝑅)
evlsaddval.k	⊢ 𝐾 = (Base‘𝑆)
evlsaddval.b	⊢ 𝐵 = (Base‘𝑃)
evlsaddval.i	⊢ (𝜑 → 𝐼 ∈ 𝑍)
evlsaddval.s	⊢ (𝜑 → 𝑆 ∈ CRing)
evlsaddval.r	⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
evlsaddval.a	⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑_m 𝐼))
evlsaddval.m	⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))
evlsexpval.g	⊢ ∙ = (._g‘(mulGrp‘𝑃))
evlsexpval.f	⊢ ↑ = (._g‘(mulGrp‘𝑆))
evlsexpval.n	⊢ (𝜑 → 𝑁 ∈ ℕ₀)

**Assertion**
Ref	Expression
evlsexpval	⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝐵 ∧ ((𝑄‘(𝑁 ∙ 𝑀))‘𝐴) = (𝑁 ↑ 𝑉)))

**Proof of Theorem evlsexpval**
Step	Hyp	Ref	Expression
1		eqid 2760	. . . 4 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
2		evlsaddval.b	. . . 4 ⊢ 𝐵 = (Base‘𝑃)
3	1, 2	mgpbas 20365	. . 3 ⊢ 𝐵 = (Base‘(mulGrp‘𝑃))
4		evlsexpval.g	. . 3 ⊢ ∙ = (._g‘(mulGrp‘𝑃))
5		evlsaddval.i	. . . . 5 ⊢ (𝜑 → 𝐼 ∈ 𝑍)
6		evlsaddval.s	. . . . 5 ⊢ (𝜑 → 𝑆 ∈ CRing)
7		evlsaddval.r	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
8		evlsaddval.q	. . . . . 6 ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
9		evlsaddval.p	. . . . . 6 ⊢ 𝑃 = (𝐼 mPoly 𝑈)
10		evlsaddval.u	. . . . . 6 ⊢ 𝑈 = (𝑆 ↾_s 𝑅)
11		eqid 2760	. . . . . 6 ⊢ (𝑆 ↑_s (𝐾 ↑_m 𝐼)) = (𝑆 ↑_s (𝐾 ↑_m 𝐼))
12		evlsaddval.k	. . . . . 6 ⊢ 𝐾 = (Base‘𝑆)
13	8, 9, 10, 11, 12	evlsrhm 22397	. . . . 5 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑃 RingHom (𝑆 ↑_s (𝐾 ↑_m 𝐼))))
14	5, 6, 7, 13	syl3anc 1398	. . . 4 ⊢ (𝜑 → 𝑄 ∈ (𝑃 RingHom (𝑆 ↑_s (𝐾 ↑_m 𝐼))))
15		rhmrcl1 20707	. . . 4 ⊢ (𝑄 ∈ (𝑃 RingHom (𝑆 ↑_s (𝐾 ↑_m 𝐼))) → 𝑃 ∈ Ring)
16	1	ringmgp 20465	. . . 4 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
17	14, 15, 16	3syl 19	. . 3 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
18		evlsexpval.n	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
19		evlsaddval.m	. . . 4 ⊢ (𝜑 → (𝑀 ∈ 𝐵 ∧ ((𝑄‘𝑀)‘𝐴) = 𝑉))
20	19	simpld 500	. . 3 ⊢ (𝜑 → 𝑀 ∈ 𝐵)
21	3, 4, 17, 18, 20	mulgnn0cld 19305	. 2 ⊢ (𝜑 → (𝑁 ∙ 𝑀) ∈ 𝐵)
22		eqid 2760	. . . . 5 ⊢ (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))
23	8, 9, 1, 4, 10, 11, 22, 12, 2, 5, 6, 7, 18, 20	evlspw 22407	. . . 4 ⊢ (𝜑 → (𝑄‘(𝑁 ∙ 𝑀)) = (𝑁(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑄‘𝑀)))
24	23	fveq1d 6887	. . 3 ⊢ (𝜑 → ((𝑄‘(𝑁 ∙ 𝑀))‘𝐴) = ((𝑁(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑄‘𝑀))‘𝐴))
25		eqid 2760	. . . 4 ⊢ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))) = (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))
26		eqid 2760	. . . 4 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
27		eqid 2760	. . . 4 ⊢ (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼)))) = (._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
28		evlsexpval.f	. . . 4 ⊢ ↑ = (._g‘(mulGrp‘𝑆))
29	6	crngringd 20473	. . . 4 ⊢ (𝜑 → 𝑆 ∈ Ring)
30		ovexd 7455	. . . 4 ⊢ (𝜑 → (𝐾 ↑_m 𝐼) ∈ V)
31	2, 25	rhmf 20715	. . . . . 6 ⊢ (𝑄 ∈ (𝑃 RingHom (𝑆 ↑_s (𝐾 ↑_m 𝐼))) → 𝑄:𝐵⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
32	14, 31	syl 18	. . . . 5 ⊢ (𝜑 → 𝑄:𝐵⟶(Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
33	32, 20	ffvelcdmd 7085	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) ∈ (Base‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))
34		evlsaddval.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ (𝐾 ↑_m 𝐼))
35	11, 25, 22, 26, 27, 28, 29, 30, 18, 33, 34	pwsexpg 20558	. . 3 ⊢ (𝜑 → ((𝑁(._g‘(mulGrp‘(𝑆 ↑_s (𝐾 ↑_m 𝐼))))(𝑄‘𝑀))‘𝐴) = (𝑁 ↑ ((𝑄‘𝑀)‘𝐴)))
36	19	simprd 501	. . . 4 ⊢ (𝜑 → ((𝑄‘𝑀)‘𝐴) = 𝑉)
37	36	oveq2d 7436	. . 3 ⊢ (𝜑 → (𝑁 ↑ ((𝑄‘𝑀)‘𝐴)) = (𝑁 ↑ 𝑉))
38	24, 35, 37	3eqtrd 2799	. 2 ⊢ (𝜑 → ((𝑄‘(𝑁 ∙ 𝑀))‘𝐴) = (𝑁 ↑ 𝑉))
39	21, 38	jca 521	1 ⊢ (𝜑 → ((𝑁 ∙ 𝑀) ∈ 𝐵 ∧ ((𝑄‘(𝑁 ∙ 𝑀))‘𝐴) = (𝑁 ↑ 𝑉)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 Vcvv 3450 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ↑_m cmap 8847 ℕ₀cn0 12606 Basecbs 17387 ↾_s cress 17408 ↑_s cpws 17617 Mndcmnd 18923 ._gcmg 19277 mulGrpcmgp 20360 Ringcrg 20459 CRingccrg 20460 RingHom crh 20699 SubRingcsubrg 20821 mPoly cmpl 22214 evalSub ces 22381

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-ofr 7694 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-er 8717 df-map 8849 df-pm 8850 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-sup 9434 df-oi 9504 df-card 10020 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-z 12694 df-dec 12815 df-uz 12966 df-fz 13640 df-fzo 13789 df-seq 14145 df-hash 14475 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-hom 17452 df-cco 17453 df-0g 17612 df-gsum 17613 df-prds 17618 df-pws 17620 df-mre 17756 df-mrc 17757 df-acs 17759 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-mhm 18978 df-submnd 18979 df-grp 19147 df-minusg 19148 df-sbg 19149 df-mulg 19278 df-subg 19333 df-ghm 19428 df-cntz 19531 df-cmn 19996 df-abl 19997 df-mgp 20361 df-rng 20375 df-ur 20408 df-srg 20413 df-ring 20461 df-cring 20462 df-rhm 20702 df-subrng 20798 df-subrg 20822 df-lmod 21137 df-lss 21207 df-lsp 21247 df-assa 22161 df-asp 22162 df-ascl 22163 df-psr 22217 df-mvr 22218 df-mpl 22219 df-evls 22383

This theorem is used by: (None)

W3C validator