Step |
Hyp |
Ref |
Expression |
1 |
|
mpfconst.b |
⊢ 𝐵 = ( Base ‘ 𝑆 ) |
2 |
|
mpfconst.q |
⊢ 𝑄 = ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) |
3 |
|
mpfconst.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
4 |
|
mpfconst.s |
⊢ ( 𝜑 → 𝑆 ∈ CRing ) |
5 |
|
mpfconst.r |
⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) |
6 |
|
mpfproj.j |
⊢ ( 𝜑 → 𝐽 ∈ 𝐼 ) |
7 |
|
eqid |
⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) |
8 |
|
eqid |
⊢ ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) = ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) |
9 |
|
eqid |
⊢ ( 𝑆 ↾s 𝑅 ) = ( 𝑆 ↾s 𝑅 ) |
10 |
7 8 9 1 3 4 5 6
|
evlsvar |
⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ‘ 𝐽 ) ) = ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑓 ‘ 𝐽 ) ) ) |
11 |
|
eqid |
⊢ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) |
12 |
|
eqid |
⊢ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) = ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) |
13 |
7 11 9 12 1
|
evlsrhm |
⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ ( SubRing ‘ 𝑆 ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) ) |
14 |
3 4 5 13
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) ) |
15 |
|
eqid |
⊢ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) = ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) |
16 |
|
eqid |
⊢ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) = ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) |
17 |
15 16
|
rhmf |
⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ∈ ( ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) RingHom ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) ) |
18 |
|
ffn |
⊢ ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) : ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ⟶ ( Base ‘ ( 𝑆 ↑s ( 𝐵 ↑m 𝐼 ) ) ) → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) |
19 |
14 17 18
|
3syl |
⊢ ( 𝜑 → ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) |
20 |
9
|
subrgring |
⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → ( 𝑆 ↾s 𝑅 ) ∈ Ring ) |
21 |
5 20
|
syl |
⊢ ( 𝜑 → ( 𝑆 ↾s 𝑅 ) ∈ Ring ) |
22 |
11 8 15 3 21 6
|
mvrcl |
⊢ ( 𝜑 → ( ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ‘ 𝐽 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) |
23 |
|
fnfvelrn |
⊢ ( ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) Fn ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ∧ ( ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ‘ 𝐽 ) ∈ ( Base ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝑅 ) ) ) ) → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ‘ 𝐽 ) ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ) |
24 |
19 22 23
|
syl2anc |
⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ‘ 𝐽 ) ) ∈ ran ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ) |
25 |
24 2
|
eleqtrrdi |
⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝑅 ) ) ‘ 𝐽 ) ) ∈ 𝑄 ) |
26 |
10 25
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑓 ‘ 𝐽 ) ) ∈ 𝑄 ) |