Metamath Proof Explorer


Theorem opsqrlem3

Description: Lemma for opsqri . (Contributed by NM, 22-Aug-2006) (New usage is discouraged.)

Ref Expression
Hypotheses opsqrlem2.1 T HrmOp
opsqrlem2.2 S = x HrmOp , y HrmOp x + op 1 2 · op T - op x x
opsqrlem2.3 F = seq 1 S × 0 hop
Assertion opsqrlem3 G HrmOp H HrmOp G S H = G + op 1 2 · op T - op G G

Proof

Step Hyp Ref Expression
1 opsqrlem2.1 T HrmOp
2 opsqrlem2.2 S = x HrmOp , y HrmOp x + op 1 2 · op T - op x x
3 opsqrlem2.3 F = seq 1 S × 0 hop
4 id z = G z = G
5 4 4 coeq12d z = G z z = G G
6 5 oveq2d z = G T - op z z = T - op G G
7 6 oveq2d z = G 1 2 · op T - op z z = 1 2 · op T - op G G
8 4 7 oveq12d z = G z + op 1 2 · op T - op z z = G + op 1 2 · op T - op G G
9 eqidd w = H G + op 1 2 · op T - op G G = G + op 1 2 · op T - op G G
10 id x = z x = z
11 10 10 coeq12d x = z x x = z z
12 11 oveq2d x = z T - op x x = T - op z z
13 12 oveq2d x = z 1 2 · op T - op x x = 1 2 · op T - op z z
14 10 13 oveq12d x = z x + op 1 2 · op T - op x x = z + op 1 2 · op T - op z z
15 eqidd y = w z + op 1 2 · op T - op z z = z + op 1 2 · op T - op z z
16 14 15 cbvmpov x HrmOp , y HrmOp x + op 1 2 · op T - op x x = z HrmOp , w HrmOp z + op 1 2 · op T - op z z
17 2 16 eqtri S = z HrmOp , w HrmOp z + op 1 2 · op T - op z z
18 ovex G + op 1 2 · op T - op G G V
19 8 9 17 18 ovmpo G HrmOp H HrmOp G S H = G + op 1 2 · op T - op G G