This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subrg1asclcl

Description: The scalars in a polynomial algebra are in the subring algebra iff the scalar value is in the subring. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses subrg1ascl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
subrg1ascl.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
subrg1ascl.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
subrg1ascl.u ⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
subrg1ascl.r ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
subrg1asclcl.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
subrg1asclcl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
subrg1asclcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
Assertion subrg1asclcl ( 𝜑 → ( ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ↔ 𝑋 ∈ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 subrg1ascl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 subrg1ascl.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
3 subrg1ascl.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
4 subrg1ascl.u ⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
5 subrg1ascl.r ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
6 subrg1asclcl.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
7 subrg1asclcl.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
8 subrg1asclcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
9 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
10 1 2 ply1ascl ⊢ 𝐴 = ( algSc ‘ ( 1o mPoly 𝑅 ) )
11 eqid ⊢ ( 1o mPoly 𝐻 ) = ( 1o mPoly 𝐻 )
12 1on ⊢ 1o ∈ On
13 12 a1i ⊢ ( 𝜑 → 1o ∈ On )
14 4 6 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
15 9 10 3 11 13 5 14 7 8 subrgasclcl ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ↔ 𝑋 ∈ 𝑇 ) )