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 \in HrmOp$
		opsqrlem2.2	$⊢ S = (x \in HrmOp, y \in HrmOp ⟼ x +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (x \circ x))))$
		opsqrlem2.3	$⊢ F = seq 1 (S, (ℕ \times \{0_{hop}\}))$
	Assertion	opsqrlem3	$⊢ (G \in HrmOp \land H \in HrmOp) \to G S H = G +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (G \circ G)))$

Proof

Step	Hyp	Ref	Expression
1		opsqrlem2.1	$⊢ T \in HrmOp$
2		opsqrlem2.2	$⊢ S = (x \in HrmOp, y \in HrmOp ⟼ x +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (x \circ x))))$
3		opsqrlem2.3	$⊢ F = seq 1 (S, (ℕ \times \{0_{hop}\}))$
4		id	$⊢ z = G \to z = G$
5	4 4	coeq12d	$⊢ z = G \to z \circ z = G \circ G$
6	5	oveq2d	$⊢ z = G \to T -_{op} (z \circ z) = T -_{op} (G \circ G)$
7	6	oveq2d	$⊢ z = G \to (\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z)) = (\frac{1}{2}) \cdot_{op} (T -_{op} (G \circ G))$
8	4 7	oveq12d	$⊢ z = G \to z +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z))) = G +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (G \circ G)))$
9		eqidd	$⊢ w = H \to G +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (G \circ G))) = G +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (G \circ G)))$
10		id	$⊢ x = z \to x = z$
11	10 10	coeq12d	$⊢ x = z \to x \circ x = z \circ z$
12	11	oveq2d	$⊢ x = z \to T -_{op} (x \circ x) = T -_{op} (z \circ z)$
13	12	oveq2d	$⊢ x = z \to (\frac{1}{2}) \cdot_{op} (T -_{op} (x \circ x)) = (\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z))$
14	10 13	oveq12d	$⊢ x = z \to x +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (x \circ x))) = z +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z)))$
15		eqidd	$⊢ y = w \to z +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z))) = z +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z)))$
16	14 15	cbvmpov	$⊢ (x \in HrmOp, y \in HrmOp ⟼ x +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (x \circ x)))) = (z \in HrmOp, w \in HrmOp ⟼ z +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z))))$
17	2 16	eqtri	$⊢ S = (z \in HrmOp, w \in HrmOp ⟼ z +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z))))$
18		ovex	$⊢ G +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (G \circ G))) \in V$
19	8 9 17 18	ovmpo	$⊢ (G \in HrmOp \land H \in HrmOp) \to G S H = G +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (G \circ G)))$