Theorem evlsval 21961

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 3485	. . . . 5 ⊢ (𝐼 ∈ 𝑍 → 𝐼 ∈ V)
3		fveq2 6882	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
4	3	adantl 481	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → (Base‘𝑠) = (Base‘𝑆))
5	4	csbeq1d 3890	. . . . . . . 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 6895	. . . . . . . . . 10 ⊢ (Base‘𝑆) ∈ V
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → (Base‘𝑆) ∈ V)
8		simplr 766	. . . . . . . . . . 11 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → 𝑠 = 𝑆)
9	8	fveq2d 6886	. . . . . . . . . 10 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (SubRing‘𝑠) = (SubRing‘𝑆))
10		simpll 764	. . . . . . . . . . . . 13 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → 𝑖 = 𝐼)
11		oveq1 7409	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑆 → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
12	11	ad2antlr 724	. . . . . . . . . . . . 13 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
13	10, 12	oveq12d 7420	. . . . . . . . . . . 12 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝑖 mPoly (𝑠 ↾s 𝑟)) = (𝐼 mPoly (𝑆 ↾s 𝑟)))
14	13	csbeq1d 3890	. . . . . . . . . . 11 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) = ⦋(𝐼 mPoly (𝑆 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))))
15		ovexd 7437	. . . . . . . . . . . 12 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝐼 mPoly (𝑆 ↾s 𝑟)) ∈ V)
16		simprr 770	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))
17		simplr 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑠 = 𝑆)
18		simprl 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑏 = (Base‘𝑆))
19		simpll 764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → 𝑖 = 𝐼)
20	18, 19	oveq12d 7420	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑏 ↑m 𝑖) = ((Base‘𝑆) ↑m 𝐼))
21	17, 20	oveq12d 7420	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑠 ↑s (𝑏 ↑m 𝑖)) = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))
22	16, 21	oveq12d 7420	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖))) = ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
23	16	fveq2d 6886	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (algSc‘𝑤) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟))))
24	23	coeq2d 5853	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑓 ∘ (algSc‘𝑤)) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))))
25	20	xpeq1d 5696	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑏 ↑m 𝑖) × {𝑥}) = (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
26	25	mpteq2dv 5241	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
27	24, 26	eqeq12d 2740	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))))
28	17	oveq1d 7417	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
29	19, 28	oveq12d 7420	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑖 mVar (𝑠 ↾s 𝑟)) = (𝐼 mVar (𝑆 ↾s 𝑟)))
30	29	coeq2d 5853	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))))
31	20	mpteq1d 5234	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)) = (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
32	19, 31	mpteq12dv 5230	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))
33	30, 32	eqeq12d 2740	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
34	27, 33	anbi12d 630	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
35	22, 34	riotaeqbidv 7361	. . . . . . . . . . . . 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 467	. . . . . . . . . . . 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 3924	. . . . . . . . . . 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 2764	. . . . . . . . . 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 5230	. . . . . . . . 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 3924	. . . . . . . 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 2764	. . . . . . 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 21947	. . . . . . 7 ⊢ evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))))
43		fvex 6895	. . . . . . . 8 ⊢ (SubRing‘𝑆) ∈ V
44	43	mptex 7217	. . . . . . 7 ⊢ (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))) ∈ V
45	41, 42, 44	ovmpoa 7556	. . . . . 6 ⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing) → (𝐼 evalSub 𝑆) = (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))))
46	45	fveq1d 6884	. . . . 5 ⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing) → ((𝐼 evalSub 𝑆)‘𝑅) = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
47	2, 46	sylan 579	. . . 4 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing) → ((𝐼 evalSub 𝑆)‘𝑅) = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
48	1, 47	eqtrid 2776	. . 3 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing) → 𝑄 = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
49	48	3adant3 1129	. 2 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
50		oveq2 7410	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑆 ↾s 𝑟) = (𝑆 ↾s 𝑅))
51	50	oveq2d 7418	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (𝐼 mPoly (𝑆 ↾s 𝑟)) = (𝐼 mPoly (𝑆 ↾s 𝑅)))
52	51	oveq1d 7417	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))) = ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
53	51	fveq2d 6886	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟))) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))))
54	53	coeq2d 5853	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))))
55		mpteq1 5232	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
56	54, 55	eqeq12d 2740	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))))
57	50	oveq2d 7418	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝐼 mVar (𝑆 ↾s 𝑟)) = (𝐼 mVar (𝑆 ↾s 𝑅)))
58	57	coeq2d 5853	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))))
59	58	eqeq1d 2726	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))) ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
60	56, 59	anbi12d 630	. . . . . 6 ⊢ (𝑟 = 𝑅 → (((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
61	52, 60	riotaeqbidv 7361	. . . . 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 2724	. . . . 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 7362	. . . . 5 ⊢ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))) ∈ V
64	61, 62, 63	fvmpt 6989	. . . 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 7413	. . . . . . . . 9 ⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly (𝑆 ↾s 𝑅))
68	65, 67	eqtri 2752	. . . . . . . 8 ⊢ 𝑊 = (𝐼 mPoly (𝑆 ↾s 𝑅))
69		evlsval.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑m 𝐼))
70		evlsval.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑆)
71	70	oveq1i 7412	. . . . . . . . . 10 ⊢ (𝐵 ↑m 𝐼) = ((Base‘𝑆) ↑m 𝐼)
72	71	oveq2i 7413	. . . . . . . . 9 ⊢ (𝑆 ↑s (𝐵 ↑m 𝐼)) = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))
73	69, 72	eqtri 2752	. . . . . . . 8 ⊢ 𝑇 = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))
74	68, 73	oveq12i 7414	. . . . . . 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 6885	. . . . . . . . . . 11 ⊢ (algSc‘𝑊) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))
78	76, 77	eqtri 2752	. . . . . . . . . 10 ⊢ 𝐴 = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))
79	78	coeq2i 5851	. . . . . . . . 9 ⊢ (𝑓 ∘ 𝐴) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))))
80		evlsval.x	. . . . . . . . . 10 ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥}))
81	71	xpeq1i 5693	. . . . . . . . . . 11 ⊢ ((𝐵 ↑m 𝐼) × {𝑥}) = (((Base‘𝑆) ↑m 𝐼) × {𝑥})
82	81	mpteq2i 5244	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
83	80, 82	eqtri 2752	. . . . . . . . 9 ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
84	79, 83	eqeq12i 2742	. . . . . . . 8 ⊢ ((𝑓 ∘ 𝐴) = 𝑋 ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
85		evlsval.v	. . . . . . . . . . 11 ⊢ 𝑉 = (𝐼 mVar 𝑈)
86	66	oveq2i 7413	. . . . . . . . . . 11 ⊢ (𝐼 mVar 𝑈) = (𝐼 mVar (𝑆 ↾s 𝑅))
87	85, 86	eqtri 2752	. . . . . . . . . 10 ⊢ 𝑉 = (𝐼 mVar (𝑆 ↾s 𝑅))
88	87	coeq2i 5851	. . . . . . . . 9 ⊢ (𝑓 ∘ 𝑉) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅)))
89		evlsval.y	. . . . . . . . . 10 ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)))
90		eqid 2724	. . . . . . . . . . . 12 ⊢ (𝑔‘𝑥) = (𝑔‘𝑥)
91	71, 90	mpteq12i 5245	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)) = (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))
92	91	mpteq2i 5244	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
93	89, 92	eqtri 2752	. . . . . . . . 9 ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
94	88, 93	eqeq12i 2742	. . . . . . . 8 ⊢ ((𝑓 ∘ 𝑉) = 𝑌 ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))
95	84, 94	anbi12i 626	. . . . . . 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 7361	. . . . 5 ⊢ (⊤ → (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
98	97	mptru 1540	. . . 4 ⊢ (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)) = (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
99	64, 98	eqtr4di 2782	. . 3 ⊢ (𝑅 ∈ (SubRing‘𝑆) → ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅) = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
100	99	3ad2ant3 1132	. 2 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅) = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
101	49, 100	eqtrd 2764	1 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533  ⊤wtru 1534   ∈ wcel 2098  Vcvv 3466  ⦋csb 3886  {csn 4621   ↦ cmpt 5222   × cxp 5665   ∘ ccom 5671  ‘cfv 6534  ℩crio 7357  (class class class)co 7402   ↑_m cmap 8817  Basecbs 17145   ↾_s cress 17174   ↑_s cpws 17393  CRingccrg 20131   RingHom crh 20363  SubRingcsubrg 20461  algSccascl 21717   mVar cmvr 21769   mPoly cmpl 21770   evalSub ces 21945

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 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pr 5418

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-evls 21947

This theorem is referenced by:  evlsval2  21962  evlsval3  41624