Theorem opsrplusgOLD

Description: Obsolete version of opsrplusg as of 1-Nov-2024. The addition operation of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	opsrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	opsrbas.o	⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
	opsrbas.t	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
Assertion	opsrplusgOLD	⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		opsrbas.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		opsrbas.o	⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
3		opsrbas.t	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
4		df-plusg	⊢ +g = Slot 2
5		2nn	⊢ 2 ∈ ℕ
6		2lt10	⊢ 2 < ; 1 0
7	1 2 3 4 5 6	opsrbaslemOLD	⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑂 ) )