Theorem evlsval 22375

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 3472	. . . . 5 ⊢ (𝐼 ∈ 𝑍 → 𝐼 ∈ V)
3		fveq2 6877	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
4	3	adantl 487	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → (Base‘𝑠) = (Base‘𝑆))
5	4	csbeq1d 3851	. . . . . . . 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 6890	. . . . . . . . . 10 ⊢ (Base‘𝑆) ∈ V
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → (Base‘𝑆) ∈ V)
8		simplr 781	. . . . . . . . . . 11 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → 𝑠 = 𝑆)
9	8	fveq2d 6881	. . . . . . . . . 10 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (SubRing‘𝑠) = (SubRing‘𝑆))
10		simpll 779	. . . . . . . . . . . . 13 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → 𝑖 = 𝐼)
11		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑆 → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
12	11	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
13	10, 12	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝑖 mPoly (𝑠 ↾s 𝑟)) = (𝐼 mPoly (𝑆 ↾s 𝑟)))
14	13	csbeq1d 3851	. . . . . . . . . . 11 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) = ⦋(𝐼 mPoly (𝑆 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))))
15		ovexd 7447	. . . . . . . . . . . 12 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝐼 mPoly (𝑆 ↾s 𝑟)) ∈ V)
16		simprr 785	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))
17		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑠 = 𝑆)
18		simprl 783	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑏 = (Base‘𝑆))
19		simpll 779	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑖 = 𝐼)
20	18, 19	oveq12d 7430	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑏 ↑m 𝑖) = ((Base‘𝑆) ↑m 𝐼))
21	17, 20	oveq12d 7430	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑠 ↑s (𝑏 ↑m 𝑖)) = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))
22	16, 21	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖))) = ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
23	16	fveq2d 6881	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (algSc‘𝑤) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟))))
24	23	coeq2d 5840	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑓 ∘ (algSc‘𝑤)) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))))
25	20	xpeq1d 5680	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑏 ↑m 𝑖) × {𝑥}) = (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
26	25	mpteq2dv 5199	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
27	24, 26	eqeq12d 2777	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))))
28	17	oveq1d 7427	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
29	19, 28	oveq12d 7430	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑖 mVar (𝑠 ↾s 𝑟)) = (𝐼 mVar (𝑆 ↾s 𝑟)))
30	29	coeq2d 5840	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))))
31	20	mpteq1d 5195	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)) = (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
32	19, 31	mpteq12dv 5192	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))
33	30, 32	eqeq12d 2777	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
34	27, 33	anbi12d 644	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
35	22, 34	riotaeqbidv 7372	. . . . . . . . . . . . 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 473	. . . . . . . . . . . 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 3883	. . . . . . . . . . 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 2796	. . . . . . . . . 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 5192	. . . . . . . . 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 3883	. . . . . . . 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 2796	. . . . . . 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 22363	. . . . . . 7 ⊢ evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))))
43		fvex 6890	. . . . . . . 8 ⊢ (SubRing‘𝑆) ∈ V
44	43	mptex 7221	. . . . . . 7 ⊢ (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))) ∈ V
45	41, 42, 44	ovmpoa 7567	. . . . . 6 ⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing) → (𝐼 evalSub 𝑆) = (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))))
46	45	fveq1d 6879	. . . . 5 ⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing) → ((𝐼 evalSub 𝑆)‘𝑅) = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
47	2, 46	sylan 592	. . . 4 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing) → ((𝐼 evalSub 𝑆)‘𝑅) = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
48	1, 47	eqtrid 2808	. . 3 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing) → 𝑄 = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
49	48	3adant3 1150	. 2 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
50		oveq2 7420	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑆 ↾s 𝑟) = (𝑆 ↾s 𝑅))
51	50	oveq2d 7428	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (𝐼 mPoly (𝑆 ↾s 𝑟)) = (𝐼 mPoly (𝑆 ↾s 𝑅)))
52	51	oveq1d 7427	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))) = ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
53	51	fveq2d 6881	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟))) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))))
54	53	coeq2d 5840	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))))
55		mpteq1 5194	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
56	54, 55	eqeq12d 2777	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))))
57	50	oveq2d 7428	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝐼 mVar (𝑆 ↾s 𝑟)) = (𝐼 mVar (𝑆 ↾s 𝑅)))
58	57	coeq2d 5840	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))))
59	58	eqeq1d 2763	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))) ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
60	56, 59	anbi12d 644	. . . . . 6 ⊢ (𝑟 = 𝑅 → (((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
61	52, 60	riotaeqbidv 7372	. . . . 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 2761	. . . . 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 7373	. . . . 5 ⊢ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))) ∈ V
64	61, 62, 63	fvmpt 6985	. . . 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 7423	. . . . . . . . 9 ⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly (𝑆 ↾s 𝑅))
68	65, 67	eqtri 2784	. . . . . . . 8 ⊢ 𝑊 = (𝐼 mPoly (𝑆 ↾s 𝑅))
69		evlsval.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑m 𝐼))
70		evlsval.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑆)
71	70	oveq1i 7422	. . . . . . . . . 10 ⊢ (𝐵 ↑m 𝐼) = ((Base‘𝑆) ↑m 𝐼)
72	71	oveq2i 7423	. . . . . . . . 9 ⊢ (𝑆 ↑s (𝐵 ↑m 𝐼)) = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))
73	69, 72	eqtri 2784	. . . . . . . 8 ⊢ 𝑇 = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))
74	68, 73	oveq12i 7424	. . . . . . 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 6880	. . . . . . . . . . 11 ⊢ (algSc‘𝑊) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))
78	76, 77	eqtri 2784	. . . . . . . . . 10 ⊢ 𝐴 = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))
79	78	coeq2i 5838	. . . . . . . . 9 ⊢ (𝑓 ∘ 𝐴) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))))
80		evlsval.x	. . . . . . . . . 10 ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥}))
81	71	xpeq1i 5677	. . . . . . . . . . 11 ⊢ ((𝐵 ↑m 𝐼) × {𝑥}) = (((Base‘𝑆) ↑m 𝐼) × {𝑥})
82	81	mpteq2i 5201	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
83	80, 82	eqtri 2784	. . . . . . . . 9 ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
84	79, 83	eqeq12i 2779	. . . . . . . 8 ⊢ ((𝑓 ∘ 𝐴) = 𝑋 ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
85		evlsval.v	. . . . . . . . . . 11 ⊢ 𝑉 = (𝐼 mVar 𝑈)
86	66	oveq2i 7423	. . . . . . . . . . 11 ⊢ (𝐼 mVar 𝑈) = (𝐼 mVar (𝑆 ↾s 𝑅))
87	85, 86	eqtri 2784	. . . . . . . . . 10 ⊢ 𝑉 = (𝐼 mVar (𝑆 ↾s 𝑅))
88	87	coeq2i 5838	. . . . . . . . 9 ⊢ (𝑓 ∘ 𝑉) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅)))
89		evlsval.y	. . . . . . . . . 10 ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)))
90		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑔‘𝑥) = (𝑔‘𝑥)
91	71, 90	mpteq12i 5202	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)) = (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))
92	91	mpteq2i 5201	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
93	89, 92	eqtri 2784	. . . . . . . . 9 ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
94	88, 93	eqeq12i 2779	. . . . . . . 8 ⊢ ((𝑓 ∘ 𝑉) = 𝑌 ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))
95	84, 94	anbi12i 640	. . . . . . 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 7372	. . . . 5 ⊢ (⊤ → (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
98	97	mptru 1577	. . . 4 ⊢ (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
99	64, 98	eqtr4di 2814	. . 3 ⊢ (𝑅 ∈ (SubRing‘𝑆) → ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅) = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
100	99	3ad2ant3 1153	. 2 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅) = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
101	49, 100	eqtrd 2796	1 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145  Vcvv 3451  ⦋csb 3847  {csn 4584   ↦ cmpt 5186   × cxp 5649   ∘ ccom 5655  ‘cfv 6531  ℩crio 7368  (class class class)co 7412   ↑_m cmap 8831  Basecbs 17367   ↾_s cress 17388   ↑_s cpws 17597  CRingccrg 20440   RingHom crh 20679  SubRingcsubrg 20801  algSccascl 22140   mVar cmvr 22193   mPoly cmpl 22194   evalSub ces 22361

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-evls 22363

This theorem is used by:  evlsval2  22376  evlsval3  22378