Metamath Proof Explorer

Theorem opsqrlem3

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

Ref Expression
Hypotheses opsqrlem2.1 ⊢ 𝑇 ∈ HrmOp
opsqrlem2.2 ⊢ 𝑆 = ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) )
opsqrlem2.3 ⊢ 𝐹 = seq 1 ( 𝑆 , ( ℕ × { 0hop } ) )
Assertion opsqrlem3 ( ( 𝐺 ∈ HrmOp ∧ 𝐻 ∈ HrmOp ) → ( 𝐺 𝑆 𝐻 ) = ( 𝐺 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝐺 ∘ 𝐺 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 opsqrlem2.1 ⊢ 𝑇 ∈ HrmOp
2 opsqrlem2.2 ⊢ 𝑆 = ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) )
3 opsqrlem2.3 ⊢ 𝐹 = seq 1 ( 𝑆 , ( ℕ × { 0hop } ) )
4 id ⊢ ( 𝑧 = 𝐺 → 𝑧 = 𝐺 )
5 4 4 coeq12d ⊢ ( 𝑧 = 𝐺 → ( 𝑧 ∘ 𝑧 ) = ( 𝐺 ∘ 𝐺 ) )
6 5 oveq2d ⊢ ( 𝑧 = 𝐺 → ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) = ( 𝑇 −op ( 𝐺 ∘ 𝐺 ) ) )
7 6 oveq2d ⊢ ( 𝑧 = 𝐺 → ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) = ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝐺 ∘ 𝐺 ) ) ) )
8 4 7 oveq12d ⊢ ( 𝑧 = 𝐺 → ( 𝑧 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ) = ( 𝐺 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝐺 ∘ 𝐺 ) ) ) ) )
9 eqidd ⊢ ( 𝑤 = 𝐻 → ( 𝐺 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝐺 ∘ 𝐺 ) ) ) ) = ( 𝐺 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝐺 ∘ 𝐺 ) ) ) ) )
10 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
11 10 10 coeq12d ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∘ 𝑥 ) = ( 𝑧 ∘ 𝑧 ) )
12 11 oveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) = ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) )
13 12 oveq2d ⊢ ( 𝑥 = 𝑧 → ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) = ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) )
14 10 13 oveq12d ⊢ ( 𝑥 = 𝑧 → ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) = ( 𝑧 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ) )
15 eqidd ⊢ ( 𝑦 = 𝑤 → ( 𝑧 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ) = ( 𝑧 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ) )
16 14 15 cbvmpov ⊢ ( 𝑥 ∈ HrmOp , 𝑦 ∈ HrmOp ↦ ( 𝑥 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑥 ∘ 𝑥 ) ) ) ) ) = ( 𝑧 ∈ HrmOp , 𝑤 ∈ HrmOp ↦ ( 𝑧 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ) )
17 2 16 eqtri ⊢ 𝑆 = ( 𝑧 ∈ HrmOp , 𝑤 ∈ HrmOp ↦ ( 𝑧 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝑧 ∘ 𝑧 ) ) ) ) )
18 ovex ⊢ ( 𝐺 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝐺 ∘ 𝐺 ) ) ) ) ∈ V
19 8 9 17 18 ovmpo ⊢ ( ( 𝐺 ∈ HrmOp ∧ 𝐻 ∈ HrmOp ) → ( 𝐺 𝑆 𝐻 ) = ( 𝐺 +op ( ( 1 / 2 ) ·op ( 𝑇 −op ( 𝐺 ∘ 𝐺 ) ) ) ) )