Metamath Proof Explorer


Theorem opsrbaslem

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 S=ImPwSerR
opsrbas.o O=IordPwSerRT
opsrbas.t φTI×I
opsrbaslem.1 E=SlotEndx
opsrbaslem.2 Endxndx
Assertion opsrbaslem φES=EO

Proof

Step Hyp Ref Expression
1 opsrbas.s S=ImPwSerR
2 opsrbas.o O=IordPwSerRT
3 opsrbas.t φTI×I
4 opsrbaslem.1 E=SlotEndx
5 opsrbaslem.2 Endxndx
6 4 5 setsnid ES=ESsSetndxO
7 eqid O=O
8 simprl φIVRVIV
9 simprr φIVRVRV
10 3 adantr φIVRVTI×I
11 1 2 7 8 9 10 opsrval2 φIVRVO=SsSetndxO
12 11 fveq2d φIVRVEO=ESsSetndxO
13 6 12 eqtr4id φIVRVES=EO
14 0fv T=
15 14 eqcomi =T
16 reldmpsr ReldommPwSer
17 16 ovprc ¬IVRVImPwSerR=
18 reldmopsr ReldomordPwSer
19 18 ovprc ¬IVRVIordPwSerR=
20 19 fveq1d ¬IVRVIordPwSerRT=T
21 15 17 20 3eqtr4a ¬IVRVImPwSerR=IordPwSerRT
22 21 1 2 3eqtr4g ¬IVRVS=O
23 22 fveq2d ¬IVRVES=EO
24 23 adantl φ¬IVRVES=EO
25 13 24 pm2.61dan φES=EO