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	$⊢ P = {Poly}_{1} (R)$
		subrg1ascl.a	$⊢ A = algSc (P)$
		subrg1ascl.h	$⊢ H = R ↾_{𝑠} T$
		subrg1ascl.u	$⊢ U = {Poly}_{1} (H)$
		subrg1ascl.r	$⊢ φ \to T \in SubRing (R)$
		subrg1asclcl.b	$⊢ B = {Base}_{U}$
		subrg1asclcl.k	$⊢ K = {Base}_{R}$
		subrg1asclcl.x	$⊢ φ \to X \in K$
	Assertion	subrg1asclcl	$⊢ φ \to (A (X) \in B \leftrightarrow X \in T)$

Proof

Step	Hyp	Ref	Expression
1		subrg1ascl.p	$⊢ P = {Poly}_{1} (R)$
2		subrg1ascl.a	$⊢ A = algSc (P)$
3		subrg1ascl.h	$⊢ H = R ↾_{𝑠} T$
4		subrg1ascl.u	$⊢ U = {Poly}_{1} (H)$
5		subrg1ascl.r	$⊢ φ \to T \in SubRing (R)$
6		subrg1asclcl.b	$⊢ B = {Base}_{U}$
7		subrg1asclcl.k	$⊢ K = {Base}_{R}$
8		subrg1asclcl.x	$⊢ φ \to X \in K$
9		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
10	1 2	ply1ascl	$⊢ A = algSc (1_{𝑜} mPoly R)$
11		eqid	$⊢ 1_{𝑜} mPoly H = 1_{𝑜} mPoly H$
12		1on	$⊢ 1_{𝑜} \in On$
13	12	a1i	$⊢ φ \to 1_{𝑜} \in On$
14	4 6	ply1bas	$⊢ B = {Base}_{(1_{𝑜} mPoly H)}$
15	9 10 3 11 13 5 14 7 8	subrgasclcl	$⊢ φ \to (A (X) \in B \leftrightarrow X \in T)$