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 ⊢ Q = I evalSub S ⁡ R
evlsval.w ⊢ W = I mPoly U
evlsval.v ⊢ V = I mVar U
evlsval.u ⊢ U = S ↾ 𝑠 R
evlsval.t ⊢ T = S ↑ 𝑠 B I
evlsval.b ⊢ B = Base S
evlsval.a ⊢ A = algSc ⁡ W
evlsval.x ⊢ X = x ∈ R ⟼ B I × x
evlsval.y ⊢ Y = x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x
Assertion evlsval ⊢ I ∈ Z ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → Q = ι f ∈ W RingHom T | f ∘ A = X ∧ f ∘ V = Y

Proof

Step Hyp Ref Expression
1 evlsval.q ⊢ Q = I evalSub S ⁡ R
2 evlsval.w ⊢ W = I mPoly U
3 evlsval.v ⊢ V = I mVar U
4 evlsval.u ⊢ U = S ↾ 𝑠 R
5 evlsval.t ⊢ T = S ↑ 𝑠 B I
6 evlsval.b ⊢ B = Base S
7 evlsval.a ⊢ A = algSc ⁡ W
8 evlsval.x ⊢ X = x ∈ R ⟼ B I × x
9 evlsval.y ⊢ Y = x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x
10 elex ⊢ I ∈ Z → I ∈ V
11 fveq2 ⊢ s = S → Base s = Base S
12 11 adantl ⊢ i = I ∧ s = S → Base s = Base S
13 12 csbeq1d ⊢ i = I ∧ s = S → ⦋ Base s / b⦌ r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = ⦋ Base S / b⦌ r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
14 fvex ⊢ Base S ∈ V
15 14 a1i ⊢ i = I ∧ s = S → Base S ∈ V
16 simplr ⊢ i = I ∧ s = S ∧ b = Base S → s = S
17 16 fveq2d ⊢ i = I ∧ s = S ∧ b = Base S → SubRing ⁡ s = SubRing ⁡ S
18 simpll ⊢ i = I ∧ s = S ∧ b = Base S → i = I
19 oveq1 ⊢ s = S → s ↾ 𝑠 r = S ↾ 𝑠 r
20 19 ad2antlr ⊢ i = I ∧ s = S ∧ b = Base S → s ↾ 𝑠 r = S ↾ 𝑠 r
21 18 20 oveq12d ⊢ i = I ∧ s = S ∧ b = Base S → i mPoly s ↾ 𝑠 r = I mPoly S ↾ 𝑠 r
22 21 csbeq1d ⊢ i = I ∧ s = S ∧ b = Base S → ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = ⦋ I mPoly S ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
23 ovexd ⊢ i = I ∧ s = S ∧ b = Base S → I mPoly S ↾ 𝑠 r ∈ V
24 simprr ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → w = I mPoly S ↾ 𝑠 r
25 simplr ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → s = S
26 simprl ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → b = Base S
27 simpll ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → i = I
28 26 27 oveq12d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → b i = Base S I
29 25 28 oveq12d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → s ↑ 𝑠 b i = S ↑ 𝑠 Base S I
30 24 29 oveq12d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → w RingHom s ↑ 𝑠 b i = I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I
31 24 fveq2d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → algSc ⁡ w = algSc ⁡ I mPoly S ↾ 𝑠 r
32 31 coeq2d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → f ∘ algSc ⁡ w = f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r
33 28 xpeq1d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → b i × x = Base S I × x
34 33 mpteq2dv ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → x ∈ r ⟼ b i × x = x ∈ r ⟼ Base S I × x
35 32 34 eqeq12d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ↔ f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x
36 25 oveq1d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → s ↾ 𝑠 r = S ↾ 𝑠 r
37 27 36 oveq12d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → i mVar s ↾ 𝑠 r = I mVar S ↾ 𝑠 r
38 37 coeq2d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → f ∘ i mVar s ↾ 𝑠 r = f ∘ I mVar S ↾ 𝑠 r
39 28 mpteq1d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → g ∈ b i ⟼ g ⁡ x = g ∈ Base S I ⟼ g ⁡ x
40 27 39 mpteq12dv ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
41 38 40 eqeq12d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x ↔ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
42 35 41 anbi12d ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x ↔ f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
43 30 42 riotaeqbidv ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
44 43 anassrs ⊢ i = I ∧ s = S ∧ b = Base S ∧ w = I mPoly S ↾ 𝑠 r → ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
45 23 44 csbied ⊢ i = I ∧ s = S ∧ b = Base S → ⦋ I mPoly S ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
46 22 45 eqtrd ⊢ i = I ∧ s = S ∧ b = Base S → ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
47 17 46 mpteq12dv ⊢ i = I ∧ s = S ∧ b = Base S → r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
48 15 47 csbied ⊢ i = I ∧ s = S → ⦋ Base S / b⦌ r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
49 13 48 eqtrd ⊢ i = I ∧ s = S → ⦋ Base s / b⦌ r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x = r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
50 df-evls ⊢ evalSub = i ∈ V , s ∈ CRing ⟼ ⦋ Base s / b⦌ r ∈ SubRing ⁡ s ⟼ ⦋ i mPoly s ↾ 𝑠 r / w⦌ ι f ∈ w RingHom s ↑ 𝑠 b i | f ∘ algSc ⁡ w = x ∈ r ⟼ b i × x ∧ f ∘ i mVar s ↾ 𝑠 r = x ∈ i ⟼ g ∈ b i ⟼ g ⁡ x
51 fvex ⊢ SubRing ⁡ S ∈ V
52 51 mptex ⊢ r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ∈ V
53 49 50 52 ovmpoa ⊢ I ∈ V ∧ S ∈ CRing → I evalSub S = r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
54 53 fveq1d ⊢ I ∈ V ∧ S ∈ CRing → I evalSub S ⁡ R = r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ⁡ R
55 10 54 sylan ⊢ I ∈ Z ∧ S ∈ CRing → I evalSub S ⁡ R = r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ⁡ R
56 1 55 syl5eq ⊢ I ∈ Z ∧ S ∈ CRing → Q = r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ⁡ R
57 56 3adant3 ⊢ I ∈ Z ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → Q = r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ⁡ R
58 oveq2 ⊢ r = R → S ↾ 𝑠 r = S ↾ 𝑠 R
59 58 oveq2d ⊢ r = R → I mPoly S ↾ 𝑠 r = I mPoly S ↾ 𝑠 R
60 59 oveq1d ⊢ r = R → I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I = I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 Base S I
61 59 fveq2d ⊢ r = R → algSc ⁡ I mPoly S ↾ 𝑠 r = algSc ⁡ I mPoly S ↾ 𝑠 R
62 61 coeq2d ⊢ r = R → f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R
63 mpteq1 ⊢ r = R → x ∈ r ⟼ Base S I × x = x ∈ R ⟼ Base S I × x
64 62 63 eqeq12d ⊢ r = R → f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ↔ f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x
65 58 oveq2d ⊢ r = R → I mVar S ↾ 𝑠 r = I mVar S ↾ 𝑠 R
66 65 coeq2d ⊢ r = R → f ∘ I mVar S ↾ 𝑠 r = f ∘ I mVar S ↾ 𝑠 R
67 66 eqeq1d ⊢ r = R → f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ↔ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
68 64 67 anbi12d ⊢ r = R → f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ↔ f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
69 60 68 riotaeqbidv ⊢ r = R → ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x = ι f ∈ I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
70 eqid ⊢ r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x = r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
71 riotaex ⊢ ι f ∈ I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ∈ V
72 69 70 71 fvmpt ⊢ R ∈ SubRing ⁡ S → r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ⁡ R = ι f ∈ I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
73 4 oveq2i ⊢ I mPoly U = I mPoly S ↾ 𝑠 R
74 2 73 eqtri ⊢ W = I mPoly S ↾ 𝑠 R
75 6 oveq1i ⊢ B I = Base S I
76 75 oveq2i ⊢ S ↑ 𝑠 B I = S ↑ 𝑠 Base S I
77 5 76 eqtri ⊢ T = S ↑ 𝑠 Base S I
78 74 77 oveq12i ⊢ W RingHom T = I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 Base S I
79 78 a1i ⊢ ⊤ → W RingHom T = I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 Base S I
80 74 fveq2i ⊢ algSc ⁡ W = algSc ⁡ I mPoly S ↾ 𝑠 R
81 7 80 eqtri ⊢ A = algSc ⁡ I mPoly S ↾ 𝑠 R
82 81 coeq2i ⊢ f ∘ A = f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R
83 75 xpeq1i ⊢ B I × x = Base S I × x
84 83 mpteq2i ⊢ x ∈ R ⟼ B I × x = x ∈ R ⟼ Base S I × x
85 8 84 eqtri ⊢ X = x ∈ R ⟼ Base S I × x
86 82 85 eqeq12i ⊢ f ∘ A = X ↔ f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x
87 4 oveq2i ⊢ I mVar U = I mVar S ↾ 𝑠 R
88 3 87 eqtri ⊢ V = I mVar S ↾ 𝑠 R
89 88 coeq2i ⊢ f ∘ V = f ∘ I mVar S ↾ 𝑠 R
90 eqid ⊢ g ⁡ x = g ⁡ x
91 75 90 mpteq12i ⊢ g ∈ B I ⟼ g ⁡ x = g ∈ Base S I ⟼ g ⁡ x
92 91 mpteq2i ⊢ x ∈ I ⟼ g ∈ B I ⟼ g ⁡ x = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
93 9 92 eqtri ⊢ Y = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
94 89 93 eqeq12i ⊢ f ∘ V = Y ↔ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
95 86 94 anbi12i ⊢ f ∘ A = X ∧ f ∘ V = Y ↔ f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
96 95 a1i ⊢ ⊤ → f ∘ A = X ∧ f ∘ V = Y ↔ f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
97 79 96 riotaeqbidv ⊢ ⊤ → ι f ∈ W RingHom T | f ∘ A = X ∧ f ∘ V = Y = ι f ∈ I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
98 97 mptru ⊢ ι f ∈ W RingHom T | f ∘ A = X ∧ f ∘ V = Y = ι f ∈ I mPoly S ↾ 𝑠 R RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 R = x ∈ R ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 R = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x
99 72 98 syl6eqr ⊢ R ∈ SubRing ⁡ S → r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ⁡ R = ι f ∈ W RingHom T | f ∘ A = X ∧ f ∘ V = Y
100 99 3ad2ant3 ⊢ I ∈ Z ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → r ∈ SubRing ⁡ S ⟼ ι f ∈ I mPoly S ↾ 𝑠 r RingHom S ↑ 𝑠 Base S I | f ∘ algSc ⁡ I mPoly S ↾ 𝑠 r = x ∈ r ⟼ Base S I × x ∧ f ∘ I mVar S ↾ 𝑠 r = x ∈ I ⟼ g ∈ Base S I ⟼ g ⁡ x ⁡ R = ι f ∈ W RingHom T | f ∘ A = X ∧ f ∘ V = Y
101 57 100 eqtrd ⊢ I ∈ Z ∧ S ∈ CRing ∧ R ∈ SubRing ⁡ S → Q = ι f ∈ W RingHom T | f ∘ A = X ∧ f ∘ V = Y