Theorem opsrassa

Description: The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	opsrcrng.o	⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
	opsrcrng.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	opsrcrng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	opsrcrng.t	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
Assertion	opsrassa	⊢ ( 𝜑 → 𝑂 ∈ AssAlg )

Proof

Step	Hyp	Ref	Expression
1		opsrcrng.o	⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
2		opsrcrng.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3		opsrcrng.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4		opsrcrng.t	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
5		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
6	5 2 3	psrassa	⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) ∈ AssAlg )
7		eqidd	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
8	5 1 4	opsrbas	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ 𝑂 ) )
9	5 1 4	opsrplusg	⊢ ( 𝜑 → ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ 𝑂 ) )
10	9	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) )
11	5 1 4	opsrmulr	⊢ ( 𝜑 → ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ 𝑂 ) )
12	11	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) )
13	5 2 3	psrsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( 𝐼 mPwSer 𝑅 ) ) )
14	5 1 4 2 3	opsrsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑂 ) )
15		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16	5 1 4	opsrvsca	⊢ ( 𝜑 → ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ·𝑠 ‘ 𝑂 ) )
17	16	oveqdr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( ·𝑠 ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( ·𝑠 ‘ 𝑂 ) 𝑦 ) )
18	7 8 10 12 13 14 15 17	assapropd	⊢ ( 𝜑 → ( ( 𝐼 mPwSer 𝑅 ) ∈ AssAlg ↔ 𝑂 ∈ AssAlg ) )
19	6 18	mpbid	⊢ ( 𝜑 → 𝑂 ∈ AssAlg )