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