Description: The third argument passed to evalSub is in the domain. (Contributed by SN, 15-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | selvval2lem2.u | ⊢ 𝑈 = ( 𝐼 mPoly 𝑅 ) | |
| selvval2lem2.t | ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 ) | ||
| selvval2lem2.c | ⊢ 𝐶 = ( algSc ‘ 𝑇 ) | ||
| selvval2lem2.d | ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) | ||
| selvval2lem2.i | ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) | ||
| selvval2lem2.j | ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 ) | ||
| selvval2lem2.r | ⊢ ( 𝜑 → 𝑅 ∈ CRing ) | ||
| Assertion | selvval2lem3 | ⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | selvval2lem2.u | ⊢ 𝑈 = ( 𝐼 mPoly 𝑅 ) | |
| 2 | selvval2lem2.t | ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 ) | |
| 3 | selvval2lem2.c | ⊢ 𝐶 = ( algSc ‘ 𝑇 ) | |
| 4 | selvval2lem2.d | ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) | |
| 5 | selvval2lem2.i | ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) | |
| 6 | selvval2lem2.j | ⊢ ( 𝜑 → 𝐽 ∈ 𝑊 ) | |
| 7 | selvval2lem2.r | ⊢ ( 𝜑 → 𝑅 ∈ CRing ) | |
| 8 | 1 2 3 4 5 6 7 | selvval2lem2 | ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) ) |
| 9 | rnrhmsubrg | ⊢ ( 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) ) | |
| 10 | 8 9 | syl | ⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) ) |