Theorem opsrsca

Description: The scalar ring of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015) (Revised by AV, 1-Nov-2024)

	Ref	Expression
Hypotheses	opsrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	opsrbas.o	⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
	opsrbas.t	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
	opsrsca.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	opsrsca.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
Assertion	opsrsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		opsrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		opsrbas.o	⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
3		opsrbas.t	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
4		opsrsca.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5		opsrsca.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
6	1 4 5	psrsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) )
7		scaid	⊢ Scalar = Slot ( Scalar ‘ ndx )
8		plendxnscandx	⊢ ( le ‘ ndx ) ≠ ( Scalar ‘ ndx )
9	8	necomi	⊢ ( Scalar ‘ ndx ) ≠ ( le ‘ ndx )
10	1 2 3 7 9	opsrbaslem	⊢ ( 𝜑 → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑂 ) )
11	6 10	eqtrd	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑂 ) )