Theorem evlsval 21496

Description: Value of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 11-Mar-2015.) (Revised by AV, 18-Sep-2021.)

Hypotheses

Ref	Expression
evlsval.q	⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
evlsval.w	⊢ 𝑊 = (𝐼 mPoly 𝑈)
evlsval.v	⊢ 𝑉 = (𝐼 mVar 𝑈)
evlsval.u	⊢ 𝑈 = (𝑆 ↾s 𝑅)
evlsval.t	⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑m 𝐼))
evlsval.b	⊢ 𝐵 = (Base‘𝑆)
evlsval.a	⊢ 𝐴 = (algSc‘𝑊)
evlsval.x	⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥}))
evlsval.y	⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)))

Assertion

Ref	Expression
evlsval	⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))

Distinct variable groups:   𝑓,𝐼,𝑔,𝑥   𝑅,𝑓,𝑥   𝑆,𝑓,𝑔,𝑥   𝑇,𝑓   𝑓,𝑊

Allowed substitution hints:   𝐴(𝑥,𝑓,𝑔)   𝐵(𝑥,𝑓,𝑔)   𝑄(𝑥,𝑓,𝑔)   𝑅(𝑔)   𝑇(𝑥,𝑔)   𝑈(𝑥,𝑓,𝑔)   𝑉(𝑥,𝑓,𝑔)   𝑊(𝑥,𝑔)   𝑋(𝑥,𝑓,𝑔)   𝑌(𝑥,𝑓,𝑔)   𝑍(𝑥,𝑓,𝑔)

Proof of Theorem evlsval

Dummy variables 𝑏 𝑖 𝑟 𝑠 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlsval.q	. . . 4 ⊢ 𝑄 = ((𝐼 evalSub 𝑆)‘𝑅)
2		elex 3463	. . . . 5 ⊢ (𝐼 ∈ 𝑍 → 𝐼 ∈ V)
3		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
4	3	adantl 482	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → (Base‘𝑠) = (Base‘𝑆))
5	4	csbeq1d 3859	. . . . . . . 8 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))) = ⦋(Base‘𝑆) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))))
6		fvex 6855	. . . . . . . . . 10 ⊢ (Base‘𝑆) ∈ V
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → (Base‘𝑆) ∈ V)
8		simplr 767	. . . . . . . . . . 11 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → 𝑠 = 𝑆)
9	8	fveq2d 6846	. . . . . . . . . 10 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (SubRing‘𝑠) = (SubRing‘𝑆))
10		simpll 765	. . . . . . . . . . . . 13 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → 𝑖 = 𝐼)
11		oveq1 7364	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑆 → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
12	11	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
13	10, 12	oveq12d 7375	. . . . . . . . . . . 12 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝑖 mPoly (𝑠 ↾s 𝑟)) = (𝐼 mPoly (𝑆 ↾s 𝑟)))
14	13	csbeq1d 3859	. . . . . . . . . . 11 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) = ⦋(𝐼 mPoly (𝑆 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))))
15		ovexd 7392	. . . . . . . . . . . 12 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝐼 mPoly (𝑆 ↾s 𝑟)) ∈ V)
16		simprr 771	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))
17		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑠 = 𝑆)
18		simprl 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑏 = (Base‘𝑆))
19		simpll 765	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑖 = 𝐼)
20	18, 19	oveq12d 7375	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑏 ↑m 𝑖) = ((Base‘𝑆) ↑m 𝐼))
21	17, 20	oveq12d 7375	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑠 ↑s (𝑏 ↑m 𝑖)) = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))
22	16, 21	oveq12d 7375	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖))) = ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
23	16	fveq2d 6846	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (algSc‘𝑤) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟))))
24	23	coeq2d 5818	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑓 ∘ (algSc‘𝑤)) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))))
25	20	xpeq1d 5662	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑏 ↑m 𝑖) × {𝑥}) = (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
26	25	mpteq2dv 5207	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
27	24, 26	eqeq12d 2752	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))))
28	17	oveq1d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
29	19, 28	oveq12d 7375	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑖 mVar (𝑠 ↾s 𝑟)) = (𝐼 mVar (𝑆 ↾s 𝑟)))
30	29	coeq2d 5818	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))))
31	20	mpteq1d 5200	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)) = (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
32	19, 31	mpteq12dv 5196	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))
33	30, 32	eqeq12d 2752	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
34	27, 33	anbi12d 631	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
35	22, 34	riotaeqbidv 7316	. . . . . . . . . . . . 13 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
36	35	anassrs 468	. . . . . . . . . . . 12 ⊢ ((((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟))) → (℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
37	15, 36	csbied 3893	. . . . . . . . . . 11 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → ⦋(𝐼 mPoly (𝑆 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
38	14, 37	eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
39	9, 38	mpteq12dv 5196	. . . . . . . . 9 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))) = (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))))
40	7, 39	csbied 3893	. . . . . . . 8 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → ⦋(Base‘𝑆) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))) = (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))))
41	5, 40	eqtrd 2776	. . . . . . 7 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))) = (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))))
42		df-evls 21482	. . . . . . 7 ⊢ evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))))
43		fvex 6855	. . . . . . . 8 ⊢ (SubRing‘𝑆) ∈ V
44	43	mptex 7173	. . . . . . 7 ⊢ (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))) ∈ V
45	41, 42, 44	ovmpoa 7510	. . . . . 6 ⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing) → (𝐼 evalSub 𝑆) = (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))))
46	45	fveq1d 6844	. . . . 5 ⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing) → ((𝐼 evalSub 𝑆)‘𝑅) = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
47	2, 46	sylan 580	. . . 4 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing) → ((𝐼 evalSub 𝑆)‘𝑅) = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
48	1, 47	eqtrid 2788	. . 3 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing) → 𝑄 = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
49	48	3adant3 1132	. 2 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
50		oveq2 7365	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑆 ↾s 𝑟) = (𝑆 ↾s 𝑅))
51	50	oveq2d 7373	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (𝐼 mPoly (𝑆 ↾s 𝑟)) = (𝐼 mPoly (𝑆 ↾s 𝑅)))
52	51	oveq1d 7372	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))) = ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
53	51	fveq2d 6846	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟))) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))))
54	53	coeq2d 5818	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))))
55		mpteq1 5198	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
56	54, 55	eqeq12d 2752	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))))
57	50	oveq2d 7373	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝐼 mVar (𝑆 ↾s 𝑟)) = (𝐼 mVar (𝑆 ↾s 𝑅)))
58	57	coeq2d 5818	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))))
59	58	eqeq1d 2738	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))) ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
60	56, 59	anbi12d 631	. . . . . 6 ⊢ (𝑟 = 𝑅 → (((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
61	52, 60	riotaeqbidv 7316	. . . . 5 ⊢ (𝑟 = 𝑅 → (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
62		eqid 2736	. . . . 5 ⊢ (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))) = (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
63		riotaex 7317	. . . . 5 ⊢ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))) ∈ V
64	61, 62, 63	fvmpt 6948	. . . 4 ⊢ (𝑅 ∈ (SubRing‘𝑆) → ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
65		evlsval.w	. . . . . . . . 9 ⊢ 𝑊 = (𝐼 mPoly 𝑈)
66		evlsval.u	. . . . . . . . . 10 ⊢ 𝑈 = (𝑆 ↾s 𝑅)
67	66	oveq2i 7368	. . . . . . . . 9 ⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly (𝑆 ↾s 𝑅))
68	65, 67	eqtri 2764	. . . . . . . 8 ⊢ 𝑊 = (𝐼 mPoly (𝑆 ↾s 𝑅))
69		evlsval.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑m 𝐼))
70		evlsval.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑆)
71	70	oveq1i 7367	. . . . . . . . . 10 ⊢ (𝐵 ↑m 𝐼) = ((Base‘𝑆) ↑m 𝐼)
72	71	oveq2i 7368	. . . . . . . . 9 ⊢ (𝑆 ↑s (𝐵 ↑m 𝐼)) = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))
73	69, 72	eqtri 2764	. . . . . . . 8 ⊢ 𝑇 = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))
74	68, 73	oveq12i 7369	. . . . . . 7 ⊢ (𝑊 RingHom 𝑇) = ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))
75	74	a1i 11	. . . . . 6 ⊢ (⊤ → (𝑊 RingHom 𝑇) = ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
76		evlsval.a	. . . . . . . . . . 11 ⊢ 𝐴 = (algSc‘𝑊)
77	68	fveq2i 6845	. . . . . . . . . . 11 ⊢ (algSc‘𝑊) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))
78	76, 77	eqtri 2764	. . . . . . . . . 10 ⊢ 𝐴 = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))
79	78	coeq2i 5816	. . . . . . . . 9 ⊢ (𝑓 ∘ 𝐴) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))))
80		evlsval.x	. . . . . . . . . 10 ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥}))
81	71	xpeq1i 5659	. . . . . . . . . . 11 ⊢ ((𝐵 ↑m 𝐼) × {𝑥}) = (((Base‘𝑆) ↑m 𝐼) × {𝑥})
82	81	mpteq2i 5210	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
83	80, 82	eqtri 2764	. . . . . . . . 9 ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
84	79, 83	eqeq12i 2754	. . . . . . . 8 ⊢ ((𝑓 ∘ 𝐴) = 𝑋 ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
85		evlsval.v	. . . . . . . . . . 11 ⊢ 𝑉 = (𝐼 mVar 𝑈)
86	66	oveq2i 7368	. . . . . . . . . . 11 ⊢ (𝐼 mVar 𝑈) = (𝐼 mVar (𝑆 ↾s 𝑅))
87	85, 86	eqtri 2764	. . . . . . . . . 10 ⊢ 𝑉 = (𝐼 mVar (𝑆 ↾s 𝑅))
88	87	coeq2i 5816	. . . . . . . . 9 ⊢ (𝑓 ∘ 𝑉) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅)))
89		evlsval.y	. . . . . . . . . 10 ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)))
90		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑔‘𝑥) = (𝑔‘𝑥)
91	71, 90	mpteq12i 5211	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)) = (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))
92	91	mpteq2i 5210	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
93	89, 92	eqtri 2764	. . . . . . . . 9 ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
94	88, 93	eqeq12i 2754	. . . . . . . 8 ⊢ ((𝑓 ∘ 𝑉) = 𝑌 ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))
95	84, 94	anbi12i 627	. . . . . . 7 ⊢ (((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
96	95	a1i 11	. . . . . 6 ⊢ (⊤ → (((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
97	75, 96	riotaeqbidv 7316	. . . . 5 ⊢ (⊤ → (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
98	97	mptru 1548	. . . 4 ⊢ (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
99	64, 98	eqtr4di 2794	. . 3 ⊢ (𝑅 ∈ (SubRing‘𝑆) → ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅) = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
100	99	3ad2ant3 1135	. 2 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅) = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
101	49, 100	eqtrd 2776	1 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  ⊤wtru 1542   ∈ wcel 2106  Vcvv 3445  ⦋csb 3855  {csn 4586   ↦ cmpt 5188   × cxp 5631   ∘ ccom 5637  ‘cfv 6496  ℩crio 7312  (class class class)co 7357   ↑_m cmap 8765  Basecbs 17083   ↾_s cress 17112   ↑_s cpws 17328  CRingccrg 19965   RingHom crh 20143  SubRingcsubrg 20218  algSccascl 21258   mVar cmvr 21307   mPoly cmpl 21308   evalSub ces 21480

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-evls 21482

This theorem is referenced by:  evlsval2  21497  evlsval3  40732