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		eqid	⊢ ( PwSer1 ‘ 𝐻 ) = ( PwSer1 ‘ 𝐻 )
15	4 14 6	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
16	9 10 3 11 13 5 15 7 8	subrgasclcl	⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝑋 ) ∈ 𝐵 ↔ 𝑋 ∈ 𝑇 ) )