Metamath Proof Explorer


Theorem seqeq3

Description: Equality theorem for the sequence builder operation. (Contributed by Mario Carneiro, 4-Sep-2013)

Ref Expression
Assertion seqeq3 F = G seq M + ˙ F = seq M + ˙ G

Proof

Step Hyp Ref Expression
1 fveq1 F = G F x + 1 = G x + 1
2 1 oveq2d F = G y + ˙ F x + 1 = y + ˙ G x + 1
3 2 opeq2d F = G x + 1 y + ˙ F x + 1 = x + 1 y + ˙ G x + 1
4 3 mpoeq3dv F = G x V , y V x + 1 y + ˙ F x + 1 = x V , y V x + 1 y + ˙ G x + 1
5 fveq1 F = G F M = G M
6 5 opeq2d F = G M F M = M G M
7 rdgeq12 x V , y V x + 1 y + ˙ F x + 1 = x V , y V x + 1 y + ˙ G x + 1 M F M = M G M rec x V , y V x + 1 y + ˙ F x + 1 M F M = rec x V , y V x + 1 y + ˙ G x + 1 M G M
8 4 6 7 syl2anc F = G rec x V , y V x + 1 y + ˙ F x + 1 M F M = rec x V , y V x + 1 y + ˙ G x + 1 M G M
9 8 imaeq1d F = G rec x V , y V x + 1 y + ˙ F x + 1 M F M ω = rec x V , y V x + 1 y + ˙ G x + 1 M G M ω
10 df-seq seq M + ˙ F = rec x V , y V x + 1 y + ˙ F x + 1 M F M ω
11 df-seq seq M + ˙ G = rec x V , y V x + 1 y + ˙ G x + 1 M G M ω
12 9 10 11 3eqtr4g F = G seq M + ˙ F = seq M + ˙ G