opsqrlem4

Description: Lemma for opsqri . (Contributed by NM, 17-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	opsqrlem4	$⊢ F : ℕ ⟶ HrmOp$

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		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
5		1zzd	$⊢ ⊤ \to 1 \in ℤ$
6		0hmop	$⊢ 0_{hop} \in HrmOp$
7	6	elexi	$⊢ 0_{hop} \in V$
8	7	fvconst2	$⊢ z \in ℕ \to (ℕ \times \{0_{hop}\}) (z) = 0_{hop}$
9	8 6	eqeltrdi	$⊢ z \in ℕ \to (ℕ \times \{0_{hop}\}) (z) \in HrmOp$
10	9	adantl	$⊢ (⊤ \land z \in ℕ) \to (ℕ \times \{0_{hop}\}) (z) \in HrmOp$
11	1 2 3	opsqrlem3	$⊢ (z \in HrmOp \land w \in HrmOp) \to z S w = z +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z)))$
12		halfre	$⊢ \frac{1}{2} \in ℝ$
13		simpl	$⊢ (z \in HrmOp \land w \in HrmOp) \to z \in HrmOp$
14		eqidd	$⊢ (z \in HrmOp \land w \in HrmOp) \to z \circ z = z \circ z$
15		hmopco	$⊢ (z \in HrmOp \land z \in HrmOp \land z \circ z = z \circ z) \to z \circ z \in HrmOp$
16	13 13 14 15	syl3anc	$⊢ (z \in HrmOp \land w \in HrmOp) \to z \circ z \in HrmOp$
17		hmopd	$⊢ (T \in HrmOp \land z \circ z \in HrmOp) \to T -_{op} (z \circ z) \in HrmOp$
18	1 16 17	sylancr	$⊢ (z \in HrmOp \land w \in HrmOp) \to T -_{op} (z \circ z) \in HrmOp$
19		hmopm	$⊢ (\frac{1}{2} \in ℝ \land T -_{op} (z \circ z) \in HrmOp) \to (\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z)) \in HrmOp$
20	12 18 19	sylancr	$⊢ (z \in HrmOp \land w \in HrmOp) \to (\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z)) \in HrmOp$
21		hmops	$⊢ (z \in HrmOp \land (\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z)) \in HrmOp) \to z +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z))) \in HrmOp$
22	20 21	syldan	$⊢ (z \in HrmOp \land w \in HrmOp) \to z +_{op} ((\frac{1}{2}) \cdot_{op} (T -_{op} (z \circ z))) \in HrmOp$
23	11 22	eqeltrd	$⊢ (z \in HrmOp \land w \in HrmOp) \to z S w \in HrmOp$
24	23	adantl	$⊢ (⊤ \land (z \in HrmOp \land w \in HrmOp)) \to z S w \in HrmOp$
25	4 5 10 24	seqf	$⊢ ⊤ \to seq 1 (S, (ℕ \times \{0_{hop}\})) : ℕ ⟶ HrmOp$
26	25	mptru	$⊢ seq 1 (S, (ℕ \times \{0_{hop}\})) : ℕ ⟶ HrmOp$
27	3	feq1i	$⊢ F : ℕ ⟶ HrmOp \leftrightarrow seq 1 (S, (ℕ \times \{0_{hop}\})) : ℕ ⟶ HrmOp$
28	26 27	mpbir	$⊢ F : ℕ ⟶ HrmOp$

Metamath Proof Explorer

Theorem opsqrlem4

Proof