Theorem evlsval 20293

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 3512	. . . . 5 ⊢ (𝐼 ∈ 𝑍 → 𝐼 ∈ V)
3		fveq2 6664	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (Base‘𝑠) = (Base‘𝑆))
4	3	adantl 484	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → (Base‘𝑠) = (Base‘𝑆))
5	4	csbeq1d 3886	. . . . . . . 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 6677	. . . . . . . . . 10 ⊢ (Base‘𝑆) ∈ V
7	6	a1i 11	. . . . . . . . 9 ⊢ ((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) → (Base‘𝑆) ∈ V)
8		simplr 767	. . . . . . . . . . 11 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → 𝑠 = 𝑆)
9	8	fveq2d 6668	. . . . . . . . . 10 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (SubRing‘𝑠) = (SubRing‘𝑆))
10		simpll 765	. . . . . . . . . . . . 13 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → 𝑖 = 𝐼)
11		oveq1 7157	. . . . . . . . . . . . . 14 ⊢ (𝑠 = 𝑆 → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
12	11	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
13	10, 12	oveq12d 7168	. . . . . . . . . . . 12 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → (𝑖 mPoly (𝑠 ↾s 𝑟)) = (𝐼 mPoly (𝑆 ↾s 𝑟)))
14	13	csbeq1d 3886	. . . . . . . . . . 11 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ 𝑏 = (Base‘𝑆)) → ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))) = ⦋(𝐼 mPoly (𝑆 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))))))
15		ovexd 7185	. . . . . . . . . . . 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 7168	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑏 ↑m 𝑖) = ((Base‘𝑆) ↑m 𝐼))
21	17, 20	oveq12d 7168	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑠 ↑s (𝑏 ↑m 𝑖)) = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))
22	16, 21	oveq12d 7168	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖))) = ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
23	16	fveq2d 6668	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (algSc‘𝑤) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟))))
24	23	coeq2d 5727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑓 ∘ (algSc‘𝑤)) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))))
25	20	xpeq1d 5578	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑏 ↑m 𝑖) × {𝑥}) = (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
26	25	mpteq2dv 5154	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
27	24, 26	eqeq12d 2837	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))))
28	17	oveq1d 7165	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑠 ↾s 𝑟) = (𝑆 ↾s 𝑟))
29	19, 28	oveq12d 7168	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑖 mVar (𝑠 ↾s 𝑟)) = (𝐼 mVar (𝑆 ↾s 𝑟)))
30	29	coeq2d 5727	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))))
31	20	mpteq1d 5147	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)) = (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
32	19, 31	mpteq12dv 5143	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))
33	30, 32	eqeq12d 2837	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → ((𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥))) ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
34	27, 33	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (((𝑖 = 𝐼 ∧ 𝑠 = 𝑆) ∧ (𝑏 = (Base‘𝑆) ∧ 𝑤 = (𝐼 mPoly (𝑆 ↾s 𝑟)))) → (((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
35	22, 34	riotaeqbidv 7111	. . . . . . . . . . . . 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 470	. . . . . . . . . . . 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 3918	. . . . . . . . . . 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 2856	. . . . . . . . . 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 5143	. . . . . . . . 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 3918	. . . . . . . 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 2856	. . . . . . 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 20280	. . . . . . 7 ⊢ evalSub = (𝑖 ∈ V, 𝑠 ∈ CRing ↦ ⦋(Base‘𝑠) / 𝑏⦌(𝑟 ∈ (SubRing‘𝑠) ↦ ⦋(𝑖 mPoly (𝑠 ↾s 𝑟)) / 𝑤⦌(℩𝑓 ∈ (𝑤 RingHom (𝑠 ↑s (𝑏 ↑m 𝑖)))((𝑓 ∘ (algSc‘𝑤)) = (𝑥 ∈ 𝑟 ↦ ((𝑏 ↑m 𝑖) × {𝑥})) ∧ (𝑓 ∘ (𝑖 mVar (𝑠 ↾s 𝑟))) = (𝑥 ∈ 𝑖 ↦ (𝑔 ∈ (𝑏 ↑m 𝑖) ↦ (𝑔‘𝑥)))))))
43		fvex 6677	. . . . . . . 8 ⊢ (SubRing‘𝑆) ∈ V
44	43	mptex 6980	. . . . . . 7 ⊢ (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))) ∈ V
45	41, 42, 44	ovmpoa 7299	. . . . . 6 ⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing) → (𝐼 evalSub 𝑆) = (𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))))
46	45	fveq1d 6666	. . . . 5 ⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing) → ((𝐼 evalSub 𝑆)‘𝑅) = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
47	2, 46	sylan 582	. . . 4 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing) → ((𝐼 evalSub 𝑆)‘𝑅) = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
48	1, 47	syl5eq 2868	. . 3 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing) → 𝑄 = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
49	48	3adant3 1128	. 2 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅))
50		oveq2 7158	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑆 ↾s 𝑟) = (𝑆 ↾s 𝑅))
51	50	oveq2d 7166	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (𝐼 mPoly (𝑆 ↾s 𝑟)) = (𝐼 mPoly (𝑆 ↾s 𝑅)))
52	51	oveq1d 7165	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))) = ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))))
53	51	fveq2d 6668	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟))) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))))
54	53	coeq2d 5727	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))))
55		mpteq1 5146	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
56	54, 55	eqeq12d 2837	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))))
57	50	oveq2d 7166	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → (𝐼 mVar (𝑆 ↾s 𝑟)) = (𝐼 mVar (𝑆 ↾s 𝑅)))
58	57	coeq2d 5727	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))))
59	58	eqeq1d 2823	. . . . . . 7 ⊢ (𝑟 = 𝑅 → ((𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))) ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))))
60	56, 59	anbi12d 632	. . . . . 6 ⊢ (𝑟 = 𝑅 → (((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))) ↔ ((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))
61	52, 60	riotaeqbidv 7111	. . . . 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 2821	. . . . 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 7112	. . . . 5 ⊢ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))) ∈ V
64	61, 62, 63	fvmpt 6762	. . . 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 7161	. . . . . . . . 9 ⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly (𝑆 ↾s 𝑅))
68	65, 67	eqtri 2844	. . . . . . . 8 ⊢ 𝑊 = (𝐼 mPoly (𝑆 ↾s 𝑅))
69		evlsval.t	. . . . . . . . 9 ⊢ 𝑇 = (𝑆 ↑s (𝐵 ↑m 𝐼))
70		evlsval.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝑆)
71	70	oveq1i 7160	. . . . . . . . . 10 ⊢ (𝐵 ↑m 𝐼) = ((Base‘𝑆) ↑m 𝐼)
72	71	oveq2i 7161	. . . . . . . . 9 ⊢ (𝑆 ↑s (𝐵 ↑m 𝐼)) = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))
73	69, 72	eqtri 2844	. . . . . . . 8 ⊢ 𝑇 = (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼))
74	68, 73	oveq12i 7162	. . . . . . 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 6667	. . . . . . . . . . 11 ⊢ (algSc‘𝑊) = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))
78	76, 77	eqtri 2844	. . . . . . . . . 10 ⊢ 𝐴 = (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))
79	78	coeq2i 5725	. . . . . . . . 9 ⊢ (𝑓 ∘ 𝐴) = (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))))
80		evlsval.x	. . . . . . . . . 10 ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥}))
81	71	xpeq1i 5575	. . . . . . . . . . 11 ⊢ ((𝐵 ↑m 𝐼) × {𝑥}) = (((Base‘𝑆) ↑m 𝐼) × {𝑥})
82	81	mpteq2i 5150	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝑅 ↦ ((𝐵 ↑m 𝐼) × {𝑥})) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
83	80, 82	eqtri 2844	. . . . . . . . 9 ⊢ 𝑋 = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥}))
84	79, 83	eqeq12i 2836	. . . . . . . 8 ⊢ ((𝑓 ∘ 𝐴) = 𝑋 ↔ (𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (𝑥 ∈ 𝑅 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})))
85		evlsval.v	. . . . . . . . . . 11 ⊢ 𝑉 = (𝐼 mVar 𝑈)
86	66	oveq2i 7161	. . . . . . . . . . 11 ⊢ (𝐼 mVar 𝑈) = (𝐼 mVar (𝑆 ↾s 𝑅))
87	85, 86	eqtri 2844	. . . . . . . . . 10 ⊢ 𝑉 = (𝐼 mVar (𝑆 ↾s 𝑅))
88	87	coeq2i 5725	. . . . . . . . 9 ⊢ (𝑓 ∘ 𝑉) = (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅)))
89		evlsval.y	. . . . . . . . . 10 ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)))
90		eqid 2821	. . . . . . . . . . . 12 ⊢ (𝑔‘𝑥) = (𝑔‘𝑥)
91	71, 90	mpteq12i 5151	. . . . . . . . . . 11 ⊢ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥)) = (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))
92	91	mpteq2i 5150	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ (𝐵 ↑m 𝐼) ↦ (𝑔‘𝑥))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
93	89, 92	eqtri 2844	. . . . . . . . 9 ⊢ 𝑌 = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥)))
94	88, 93	eqeq12i 2836	. . . . . . . 8 ⊢ ((𝑓 ∘ 𝑉) = 𝑌 ↔ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑅))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))
95	84, 94	anbi12i 628	. . . . . . 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 7111	. . . . 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	syl6eqr 2874	. . 3 ⊢ (𝑅 ∈ (SubRing‘𝑆) → ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅) = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
100	99	3ad2ant3 1131	. 2 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝑟 ∈ (SubRing‘𝑆) ↦ (℩𝑓 ∈ ((𝐼 mPoly (𝑆 ↾s 𝑟)) RingHom (𝑆 ↑s ((Base‘𝑆) ↑m 𝐼)))((𝑓 ∘ (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑟)))) = (𝑥 ∈ 𝑟 ↦ (((Base‘𝑆) ↑m 𝐼) × {𝑥})) ∧ (𝑓 ∘ (𝐼 mVar (𝑆 ↾s 𝑟))) = (𝑥 ∈ 𝐼 ↦ (𝑔 ∈ ((Base‘𝑆) ↑m 𝐼) ↦ (𝑔‘𝑥))))))‘𝑅) = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))
101	49, 100	eqtrd 2856	1 ⊢ ((𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → 𝑄 = (℩𝑓 ∈ (𝑊 RingHom 𝑇)((𝑓 ∘ 𝐴) = 𝑋 ∧ (𝑓 ∘ 𝑉) = 𝑌)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1533  ⊤wtru 1534   ∈ wcel 2110  Vcvv 3494  ⦋csb 3882  {csn 4560   ↦ cmpt 5138   × cxp 5547   ∘ ccom 5553  ‘cfv 6349  ℩crio 7107  (class class class)co 7150   ↑_m cmap 8400  Basecbs 16477   ↾_s cress 16478   ↑_s cpws 16714  CRingccrg 19292   RingHom crh 19458  SubRingcsubrg 19525  algSccascl 20078   mVar cmvr 20126   mPoly cmpl 20127   evalSub ces 20278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-evls 20280

This theorem is referenced by:  evlsval2  20294