ressply1evl - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ressply1evl		Structured version Visualization version GIF version

Theorem ressply1evl 33156

Description: Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025.)

**Hypotheses**
Ref	Expression
ressply1evl.q	⊢ 𝑄 = (𝑆 evalSub₁ 𝑅)
ressply1evl.k	⊢ 𝐾 = (Base‘𝑆)
ressply1evl.w	⊢ 𝑊 = (Poly₁‘𝑈)
ressply1evl.u	⊢ 𝑈 = (𝑆 ↾_s 𝑅)
ressply1evl.b	⊢ 𝐵 = (Base‘𝑊)
ressply1evl.e	⊢ 𝐸 = (eval₁‘𝑆)
ressply1evl.s	⊢ (𝜑 → 𝑆 ∈ CRing)
ressply1evl.r	⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))

**Assertion**
Ref	Expression
ressply1evl	⊢ (𝜑 → 𝑄 = (𝐸 ↾ 𝐵))

Proof of Theorem ressply1evl Dummy variables 𝑘 𝑚 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ressply1evl.e	. . . . . . 7 ⊢ 𝐸 = (eval₁‘𝑆)
2		ressply1evl.k	. . . . . . 7 ⊢ 𝐾 = (Base‘𝑆)
3	1, 2	evl1fval1 22205	. . . . . 6 ⊢ 𝐸 = (𝑆 evalSub₁ 𝐾)
4		eqid 2726	. . . . . 6 ⊢ (Poly₁‘(𝑆 ↾_s 𝐾)) = (Poly₁‘(𝑆 ↾_s 𝐾))
5		eqid 2726	. . . . . 6 ⊢ (𝑆 ↾_s 𝐾) = (𝑆 ↾_s 𝐾)
6		eqid 2726	. . . . . 6 ⊢ (Base‘(Poly₁‘(𝑆 ↾_s 𝐾))) = (Base‘(Poly₁‘(𝑆 ↾_s 𝐾)))
7		ressply1evl.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ CRing)
8	7	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → 𝑆 ∈ CRing)
9	7	crngringd 20151	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ Ring)
10	2	subrgid 20475	. . . . . . . 8 ⊢ (𝑆 ∈ Ring → 𝐾 ∈ (SubRing‘𝑆))
11	9, 10	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ (SubRing‘𝑆))
12	11	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → 𝐾 ∈ (SubRing‘𝑆))
13		eqid 2726	. . . . . . . . . 10 ⊢ (Poly₁‘𝑆) = (Poly₁‘𝑆)
14		ressply1evl.u	. . . . . . . . . 10 ⊢ 𝑈 = (𝑆 ↾_s 𝑅)
15		ressply1evl.w	. . . . . . . . . 10 ⊢ 𝑊 = (Poly₁‘𝑈)
16		ressply1evl.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑊)
17		ressply1evl.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
18		eqid 2726	. . . . . . . . . 10 ⊢ (PwSer₁‘𝑈) = (PwSer₁‘𝑈)
19		eqid 2726	. . . . . . . . . 10 ⊢ (Base‘(PwSer₁‘𝑈)) = (Base‘(PwSer₁‘𝑈))
20		eqid 2726	. . . . . . . . . 10 ⊢ (Base‘(Poly₁‘𝑆)) = (Base‘(Poly₁‘𝑆))
21	13, 14, 15, 16, 17, 18, 19, 20	ressply1bas2 22101	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 = ((Base‘(PwSer₁‘𝑈)) ∩ (Base‘(Poly₁‘𝑆))))
22		inss2 4224	. . . . . . . . 9 ⊢ ((Base‘(PwSer₁‘𝑈)) ∩ (Base‘(Poly₁‘𝑆))) ⊆ (Base‘(Poly₁‘𝑆))
23	21, 22	eqsstrdi 4031	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ (Base‘(Poly₁‘𝑆)))
24	2	ressid 17198	. . . . . . . . . . 11 ⊢ (𝑆 ∈ CRing → (𝑆 ↾_s 𝐾) = 𝑆)
25	7, 24	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝑆 ↾_s 𝐾) = 𝑆)
26	25	fveq2d 6889	. . . . . . . . 9 ⊢ (𝜑 → (Poly₁‘(𝑆 ↾_s 𝐾)) = (Poly₁‘𝑆))
27	26	fveq2d 6889	. . . . . . . 8 ⊢ (𝜑 → (Base‘(Poly₁‘(𝑆 ↾_s 𝐾))) = (Base‘(Poly₁‘𝑆)))
28	23, 27	sseqtrrd 4018	. . . . . . 7 ⊢ (𝜑 → 𝐵 ⊆ (Base‘(Poly₁‘(𝑆 ↾_s 𝐾))))
29	28	sselda 3977	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → 𝑚 ∈ (Base‘(Poly₁‘(𝑆 ↾_s 𝐾))))
30		eqid 2726	. . . . . 6 ⊢ (._r‘𝑆) = (._r‘𝑆)
31		eqid 2726	. . . . . 6 ⊢ (._g‘(mulGrp‘𝑆)) = (._g‘(mulGrp‘𝑆))
32		eqid 2726	. . . . . 6 ⊢ (coe₁‘𝑚) = (coe₁‘𝑚)
33	3, 2, 4, 5, 6, 8, 12, 29, 30, 31, 32	evls1fpws 33155	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → (𝐸‘𝑚) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σ_g (𝑘 ∈ ℕ₀ ↦ (((coe₁‘𝑚)‘𝑘)(._r‘𝑆)(𝑘(._g‘(mulGrp‘𝑆))𝑥))))))
34		ressply1evl.q	. . . . . 6 ⊢ 𝑄 = (𝑆 evalSub₁ 𝑅)
35	17	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → 𝑅 ∈ (SubRing‘𝑆))
36		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → 𝑚 ∈ 𝐵)
37	34, 2, 15, 14, 16, 8, 35, 36, 30, 31, 32	evls1fpws 33155	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → (𝑄‘𝑚) = (𝑥 ∈ 𝐾 ↦ (𝑆 Σ_g (𝑘 ∈ ℕ₀ ↦ (((coe₁‘𝑚)‘𝑘)(._r‘𝑆)(𝑘(._g‘(mulGrp‘𝑆))𝑥))))))
38	33, 37	eqtr4d 2769	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ 𝐵) → (𝐸‘𝑚) = (𝑄‘𝑚))
39	38	ralrimiva 3140	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ 𝐵 (𝐸‘𝑚) = (𝑄‘𝑚))
40		eqid 2726	. . . . . . 7 ⊢ (𝑆 ↑_s 𝐾) = (𝑆 ↑_s 𝐾)
41	1, 13, 40, 2	evl1rhm 22206	. . . . . 6 ⊢ (𝑆 ∈ CRing → 𝐸 ∈ ((Poly₁‘𝑆) RingHom (𝑆 ↑_s 𝐾)))
42		eqid 2726	. . . . . . 7 ⊢ (Base‘(𝑆 ↑_s 𝐾)) = (Base‘(𝑆 ↑_s 𝐾))
43	20, 42	rhmf 20387	. . . . . 6 ⊢ (𝐸 ∈ ((Poly₁‘𝑆) RingHom (𝑆 ↑_s 𝐾)) → 𝐸:(Base‘(Poly₁‘𝑆))⟶(Base‘(𝑆 ↑_s 𝐾)))
44	7, 41, 43	3syl 18	. . . . 5 ⊢ (𝜑 → 𝐸:(Base‘(Poly₁‘𝑆))⟶(Base‘(𝑆 ↑_s 𝐾)))
45	44	ffnd 6712	. . . 4 ⊢ (𝜑 → 𝐸 Fn (Base‘(Poly₁‘𝑆)))
46	34, 2, 40, 14, 15	evls1rhm 22196	. . . . . . 7 ⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 ∈ (𝑊 RingHom (𝑆 ↑_s 𝐾)))
47	7, 17, 46	syl2anc 583	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ (𝑊 RingHom (𝑆 ↑_s 𝐾)))
48	16, 42	rhmf 20387	. . . . . 6 ⊢ (𝑄 ∈ (𝑊 RingHom (𝑆 ↑_s 𝐾)) → 𝑄:𝐵⟶(Base‘(𝑆 ↑_s 𝐾)))
49	47, 48	syl 17	. . . . 5 ⊢ (𝜑 → 𝑄:𝐵⟶(Base‘(𝑆 ↑_s 𝐾)))
50	49	ffnd 6712	. . . 4 ⊢ (𝜑 → 𝑄 Fn 𝐵)
51		fvreseq1 7034	. . . 4 ⊢ (((𝐸 Fn (Base‘(Poly₁‘𝑆)) ∧ 𝑄 Fn 𝐵) ∧ 𝐵 ⊆ (Base‘(Poly₁‘𝑆))) → ((𝐸 ↾ 𝐵) = 𝑄 ↔ ∀𝑚 ∈ 𝐵 (𝐸‘𝑚) = (𝑄‘𝑚)))
52	45, 50, 23, 51	syl21anc 835	. . 3 ⊢ (𝜑 → ((𝐸 ↾ 𝐵) = 𝑄 ↔ ∀𝑚 ∈ 𝐵 (𝐸‘𝑚) = (𝑄‘𝑚)))
53	39, 52	mpbird 257	. 2 ⊢ (𝜑 → (𝐸 ↾ 𝐵) = 𝑄)
54	53	eqcomd 2732	1 ⊢ (𝜑 → 𝑄 = (𝐸 ↾ 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ∀wral 3055 ∩ cin 3942 ⊆ wss 3943 ↦ cmpt 5224 ↾ cres 5671 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7405 ℕ₀cn0 12476 Basecbs 17153 ↾_s cress 17182 ._rcmulr 17207 Σ_g cgsu 17395 ↑_s cpws 17401 ._gcmg 18995 mulGrpcmgp 20039 Ringcrg 20138 CRingccrg 20139 RingHom crh 20371 SubRingcsubrg 20469 PwSer₁cps1 22049 Poly₁cpl1 22051 coe₁cco1 22052 evalSub₁ ces1 22187 eval₁ce1 22188

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-tp 4628 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-iin 4993 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-se 5625 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6294 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7667 df-ofr 7668 df-om 7853 df-1st 7974 df-2nd 7975 df-supp 8147 df-frecs 8267 df-wrecs 8298 df-recs 8372 df-rdg 8411 df-1o 8467 df-er 8705 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9364 df-sup 9439 df-oi 9507 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-2 12279 df-3 12280 df-4 12281 df-5 12282 df-6 12283 df-7 12284 df-8 12285 df-9 12286 df-n0 12477 df-z 12563 df-dec 12682 df-uz 12827 df-fz 13491 df-fzo 13634 df-seq 13973 df-hash 14296 df-struct 17089 df-sets 17106 df-slot 17124 df-ndx 17136 df-base 17154 df-ress 17183 df-plusg 17219 df-mulr 17220 df-sca 17222 df-vsca 17223 df-ip 17224 df-tset 17225 df-ple 17226 df-ds 17228 df-hom 17230 df-cco 17231 df-0g 17396 df-gsum 17397 df-prds 17402 df-pws 17404 df-mre 17539 df-mrc 17540 df-acs 17542 df-mgm 18573 df-sgrp 18652 df-mnd 18668 df-mhm 18713 df-submnd 18714 df-grp 18866 df-minusg 18867 df-sbg 18868 df-mulg 18996 df-subg 19050 df-ghm 19139 df-cntz 19233 df-cmn 19702 df-abl 19703 df-mgp 20040 df-rng 20058 df-ur 20087 df-srg 20092 df-ring 20140 df-cring 20141 df-rhm 20374 df-subrng 20446 df-subrg 20471 df-lmod 20708 df-lss 20779 df-lsp 20819 df-assa 21748 df-asp 21749 df-ascl 21750 df-psr 21803 df-mvr 21804 df-mpl 21805 df-opsr 21807 df-evls 21977 df-evl 21978 df-psr1 22054 df-vr1 22055 df-ply1 22056 df-coe1 22057 df-evls1 22189 df-evl1 22190

This theorem is referenced by: evls1addd 33157 evls1subd 33158 evls1muld 33159 evls1vsca 33160 irngss 33270 evls1fvcl 33277 evls1maprhm 33278

W3C validator