Theorem psr1sca

Description: Scalars of a univariate power series ring. (Contributed by Stefan O'Rear, 4-Jul-2015)

	Ref	Expression
Hypothesis	psr1lmod.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
Assertion	psr1sca	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		psr1lmod.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
2		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
3	1	psr1val	⊢ 𝑃 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
4		0ss	⊢ ∅ ⊆ ( 1o × 1o )
5	4	a1i	⊢ ( 𝑅 ∈ 𝑉 → ∅ ⊆ ( 1o × 1o ) )
6		1on	⊢ 1o ∈ On
7	6	a1i	⊢ ( 𝑅 ∈ 𝑉 → 1o ∈ On )
8		id	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ 𝑉 )
9	2 3 5 7 8	opsrsca	⊢ ( 𝑅 ∈ 𝑉 → 𝑅 = ( Scalar ‘ 𝑃 ) )