Theorem psr1plusg

Description: Value of addition in a univariate power series ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	psr1plusg.y	⊢ 𝑌 = ( PwSer1 ‘ 𝑅 )
	psr1plusg.s	⊢ 𝑆 = ( 1o mPwSer 𝑅 )
	psr1plusg.p	⊢ + = ( +g ‘ 𝑌 )
Assertion	psr1plusg	⊢ + = ( +g ‘ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		psr1plusg.y	⊢ 𝑌 = ( PwSer1 ‘ 𝑅 )
2		psr1plusg.s	⊢ 𝑆 = ( 1o mPwSer 𝑅 )
3		psr1plusg.p	⊢ + = ( +g ‘ 𝑌 )
4	1	psr1val	⊢ 𝑌 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ )
5		0ss	⊢ ∅ ⊆ ( 1o × 1o )
6	5	a1i	⊢ ( ⊤ → ∅ ⊆ ( 1o × 1o ) )
7	2 4 6	opsrplusg	⊢ ( ⊤ → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑌 ) )
8	7	mptru	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑌 )
9	3 8	eqtr4i	⊢ + = ( +g ‘ 𝑆 )