Theorem psr1mulr

Description: Value of multiplication 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 𝑅 )
	psr1mulr.n	⊢ · = ( .r ‘ 𝑌 )
Assertion	psr1mulr	⊢ · = ( .r ‘ 𝑆 )

Proof

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