Description: The ring of ordered power series is an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opsrcrng.o | |
|
opsrcrng.i | |
||
opsrcrng.r | |
||
opsrcrng.t | |
||
Assertion | opsrassa | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opsrcrng.o | |
|
2 | opsrcrng.i | |
|
3 | opsrcrng.r | |
|
4 | opsrcrng.t | |
|
5 | eqid | |
|
6 | 5 2 3 | psrassa | |
7 | eqidd | |
|
8 | 5 1 4 | opsrbas | |
9 | 5 1 4 | opsrplusg | |
10 | 9 | oveqdr | |
11 | 5 1 4 | opsrmulr | |
12 | 11 | oveqdr | |
13 | 5 2 3 | psrsca | |
14 | 5 1 4 2 3 | opsrsca | |
15 | eqid | |
|
16 | 5 1 4 | opsrvsca | |
17 | 16 | oveqdr | |
18 | 7 8 10 12 13 14 15 17 | assapropd | |
19 | 6 18 | mpbid | |