Metamath Proof Explorer


Theorem seqomeq12

Description: Equality theorem for seqom . (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion seqomeq12 A=BC=DseqωAC=seqωBD

Proof

Step Hyp Ref Expression
1 oveq A=BaAb=aBb
2 1 opeq2d A=BsucaaAb=sucaaBb
3 2 mpoeq3dv A=Baω,bVsucaaAb=aω,bVsucaaBb
4 fveq2 C=DIC=ID
5 4 opeq2d C=DIC=ID
6 rdgeq12 aω,bVsucaaAb=aω,bVsucaaBbIC=IDrecaω,bVsucaaAbIC=recaω,bVsucaaBbID
7 3 5 6 syl2an A=BC=Drecaω,bVsucaaAbIC=recaω,bVsucaaBbID
8 7 imaeq1d A=BC=Drecaω,bVsucaaAbICω=recaω,bVsucaaBbIDω
9 df-seqom seqωAC=recaω,bVsucaaAbICω
10 df-seqom seqωBD=recaω,bVsucaaBbIDω
11 8 9 10 3eqtr4g A=BC=DseqωAC=seqωBD