Metamath Proof Explorer

Theorem evlsval

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

Ref Expression
Hypotheses 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 evlsval ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ℩ 𝑓 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑓 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑓 ∘ 𝑉 ) = 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 evlsval.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2 evlsval.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
3 evlsval.v ⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
4 evlsval.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 evlsval.t ⊢ 𝑇 = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) )
6 evlsval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
7 evlsval.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
8 evlsval.x ⊢ 𝑋 = ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) )
9 evlsval.y ⊢ 𝑌 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
10 elex ⊢ ( 𝐼 ∈ 𝑍 → 𝐼 ∈ V )
11 fveq2 ⊢ ( 𝑠 = 𝑆 → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
12 11 adantl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑠 ) = ( Base ‘ 𝑆 ) )
13 12 csbeq1d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) = ⦋ ( Base ‘ 𝑆 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )
14 fvex ⊢ ( Base ‘ 𝑆 ) ∈ V
15 14 a1i ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ( Base ‘ 𝑆 ) ∈ V )
16 simplr ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( Base ‘ 𝑆 ) ) → 𝑠 = 𝑆 )
17 16 fveq2d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( Base ‘ 𝑆 ) ) → ( SubRing ‘ 𝑠 ) = ( SubRing ‘ 𝑆 ) )
18 simpll ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( Base ‘ 𝑆 ) ) → 𝑖 = 𝐼 )
19 oveq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ↾s 𝑟 ) = ( 𝑆 ↾s 𝑟 ) )
20 19 ad2antlr ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( Base ‘ 𝑆 ) ) → ( 𝑠 ↾s 𝑟 ) = ( 𝑆 ↾s 𝑟 ) )
21 18 20 oveq12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( Base ‘ 𝑆 ) ) → ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) )
22 21 csbeq1d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( Base ‘ 𝑆 ) ) → ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) = ⦋ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
23 ovexd ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( Base ‘ 𝑆 ) ) → ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ∈ V )
24 simprr ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) )
25 simplr ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → 𝑠 = 𝑆 )
26 simprl ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → 𝑏 = ( Base ‘ 𝑆 ) )
27 simpll ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → 𝑖 = 𝐼 )
28 26 27 oveq12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑏 ↑m 𝑖 ) = ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) )
29 25 28 oveq12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) = ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) )
30 24 29 oveq12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) = ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
31 24 fveq2d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( algSc ‘ 𝑤 ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) )
32 31 coeq2d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) )
33 28 xpeq1d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) = ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) )
34 33 mpteq2dv ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) )
35 32 34 eqeq12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ↔ ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ) )
36 25 oveq1d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑠 ↾s 𝑟 ) = ( 𝑆 ↾s 𝑟 ) )
37 27 36 oveq12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) = ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) )
38 37 coeq2d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) )
39 28 mpteq1d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) = ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
40 27 39 mpteq12dv ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) )
41 38 40 eqeq12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ↔ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) )
42 35 41 anbi12d ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( Base ‘ 𝑆 ) ∧ 𝑤 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) → ( ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ↔ ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
43 30 42 riotaeqbidv ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ ( 𝑏 = ( 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
44 43 anassrs ⊢ ( ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
45 23 44 csbied ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
46 22 45 eqtrd ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
47 17 46 mpteq12dv ⊢ ( ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) ∧ 𝑏 = ( 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )
48 15 47 csbied ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )
49 13 48 eqtrd ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑠 = 𝑆 ) → ⦋ ( 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )
50 df-evls ⊢ evalSub = ( 𝑖 ∈ V , 𝑠 ∈ CRing ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )
51 fvex ⊢ ( SubRing ‘ 𝑆 ) ∈ V
52 51 mptex ⊢ ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ∈ V
53 49 50 52 ovmpoa ⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) → ( 𝐼 evalSub 𝑆 ) = ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )
54 53 fveq1d ⊢ ( ( 𝐼 ∈ V ∧ 𝑆 ∈ CRing ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ‘ 𝑅 ) )
55 10 54 sylan ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ‘ 𝑅 ) )
56 1 55 eqtrid ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ) → 𝑄 = ( ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ‘ 𝑅 ) )
57 56 3adant3 ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ‘ 𝑅 ) )
58 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑆 ↾s 𝑟 ) = ( 𝑆 ↾s 𝑅 ) )
59 58 oveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) )
60 59 oveq1d ⊢ ( 𝑟 = 𝑅 → ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) = ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
61 59 fveq2d ⊢ ( 𝑟 = 𝑅 → ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
62 61 coeq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) )
63 mpteq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) )
64 62 63 eqeq12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ↔ ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ) )
65 58 oveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) = ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) )
66 65 coeq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ) )
67 66 eqeq1d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ↔ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) )
68 64 67 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ↔ ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
69 60 68 riotaeqbidv ⊢ ( 𝑟 = 𝑅 → ( ℩ 𝑓 ∈ ( ( 𝐼 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
70 eqid ⊢ ( 𝑟 ∈ ( 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
71 riotaex ⊢ ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ∈ V
72 69 70 71 fvmpt ⊢ ( 𝑅 ∈ ( 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 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
73 4 oveq2i ⊢ ( 𝐼 mPoly 𝑈 ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) )
74 2 73 eqtri ⊢ 𝑊 = ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) )
75 6 oveq1i ⊢ ( 𝐵 ↑m 𝐼 ) = ( ( Base ‘ 𝑆 ) ↑m 𝐼 )
76 75 oveq2i ⊢ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) )
77 5 76 eqtri ⊢ 𝑇 = ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) )
78 74 77 oveq12i ⊢ ( 𝑊 RingHom 𝑇 ) = ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) )
79 78 a1i ⊢ ( ⊤ → ( 𝑊 RingHom 𝑇 ) = ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) )
80 74 fveq2i ⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) )
81 7 80 eqtri ⊢ 𝐴 = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) )
82 81 coeq2i ⊢ ( 𝑓 ∘ 𝐴 ) = ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) )
83 75 xpeq1i ⊢ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) = ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } )
84 83 mpteq2i ⊢ ( 𝑥 ∈ 𝑅 ↦ ( ( 𝐵 ↑m 𝐼 ) × { 𝑥 } ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) )
85 8 84 eqtri ⊢ 𝑋 = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) )
86 82 85 eqeq12i ⊢ ( ( 𝑓 ∘ 𝐴 ) = 𝑋 ↔ ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) )
87 4 oveq2i ⊢ ( 𝐼 mVar 𝑈 ) = ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) )
88 3 87 eqtri ⊢ 𝑉 = ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) )
89 88 coeq2i ⊢ ( 𝑓 ∘ 𝑉 ) = ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) )
90 eqid ⊢ ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 )
91 75 90 mpteq12i ⊢ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) = ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) )
92 91 mpteq2i ⊢ ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
93 9 92 eqtri ⊢ 𝑌 = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) )
94 89 93 eqeq12i ⊢ ( ( 𝑓 ∘ 𝑉 ) = 𝑌 ↔ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) )
95 86 94 anbi12i ⊢ ( ( ( 𝑓 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑓 ∘ 𝑉 ) = 𝑌 ) ↔ ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) )
96 95 a1i ⊢ ( ⊤ → ( ( ( 𝑓 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑓 ∘ 𝑉 ) = 𝑌 ) ↔ ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
97 79 96 riotaeqbidv ⊢ ( ⊤ → ( ℩ 𝑓 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑓 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑓 ∘ 𝑉 ) = 𝑌 ) ) = ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) )
98 97 mptru ⊢ ( ℩ 𝑓 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑓 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑓 ∘ 𝑉 ) = 𝑌 ) ) = ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) = ( 𝑥 ∈ 𝑅 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) )
99 72 98 eqtr4di ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ‘ 𝑅 ) = ( ℩ 𝑓 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑓 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑓 ∘ 𝑉 ) = 𝑌 ) ) )
100 99 3ad2ant3 ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝑟 ∈ ( SubRing ‘ 𝑆 ) ↦ ( ℩ 𝑓 ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) RingHom ( 𝑆 ↑s ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑟 ) ) ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝐼 mVar ( 𝑆 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 𝑔 ∈ ( ( Base ‘ 𝑆 ) ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) ‘ 𝑅 ) = ( ℩ 𝑓 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑓 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑓 ∘ 𝑉 ) = 𝑌 ) ) )
101 57 100 eqtrd ⊢ ( ( 𝐼 ∈ 𝑍 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → 𝑄 = ( ℩ 𝑓 ∈ ( 𝑊 RingHom 𝑇 ) ( ( 𝑓 ∘ 𝐴 ) = 𝑋 ∧ ( 𝑓 ∘ 𝑉 ) = 𝑌 ) ) )