Description: Get a component of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 2-Oct-2015) (Revised by AV, 9-Sep-2021) (Revised by AV, 1-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opsrbas.s | |
|
opsrbas.o | |
||
opsrbas.t | |
||
opsrbaslem.1 | |
||
opsrbaslem.2 | |
||
Assertion | opsrbaslem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opsrbas.s | |
|
2 | opsrbas.o | |
|
3 | opsrbas.t | |
|
4 | opsrbaslem.1 | |
|
5 | opsrbaslem.2 | |
|
6 | 4 5 | setsnid | |
7 | eqid | |
|
8 | simprl | |
|
9 | simprr | |
|
10 | 3 | adantr | |
11 | 1 2 7 8 9 10 | opsrval2 | |
12 | 11 | fveq2d | |
13 | 6 12 | eqtr4id | |
14 | 0fv | |
|
15 | 14 | eqcomi | |
16 | reldmpsr | |
|
17 | 16 | ovprc | |
18 | reldmopsr | |
|
19 | 18 | ovprc | |
20 | 19 | fveq1d | |
21 | 15 17 20 | 3eqtr4a | |
22 | 21 1 2 | 3eqtr4g | |
23 | 22 | fveq2d | |
24 | 23 | adantl | |
25 | 13 24 | pm2.61dan | |