Metamath Proof Explorer


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 O=IordPwSerRT
opsrcrng.i φIV
opsrcrng.r φRCRing
opsrcrng.t φTI×I
Assertion opsrassa φOAssAlg

Proof

Step Hyp Ref Expression
1 opsrcrng.o O=IordPwSerRT
2 opsrcrng.i φIV
3 opsrcrng.r φRCRing
4 opsrcrng.t φTI×I
5 eqid ImPwSerR=ImPwSerR
6 5 2 3 psrassa φImPwSerRAssAlg
7 eqidd φBaseImPwSerR=BaseImPwSerR
8 5 1 4 opsrbas φBaseImPwSerR=BaseO
9 5 1 4 opsrplusg φ+ImPwSerR=+O
10 9 oveqdr φxBaseImPwSerRyBaseImPwSerRx+ImPwSerRy=x+Oy
11 5 1 4 opsrmulr φImPwSerR=O
12 11 oveqdr φxBaseImPwSerRyBaseImPwSerRxImPwSerRy=xOy
13 5 2 3 psrsca φR=ScalarImPwSerR
14 5 1 4 2 3 opsrsca φR=ScalarO
15 eqid BaseR=BaseR
16 5 1 4 opsrvsca φImPwSerR=O
17 16 oveqdr φxBaseRyBaseImPwSerRxImPwSerRy=xOy
18 7 8 10 12 13 14 15 17 assapropd φImPwSerRAssAlgOAssAlg
19 6 18 mpbid φOAssAlg