Proof of Theorem lnopeq0lem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝑇‘𝐴) = (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) | 
| 2 | 1 | oveq1d 7446 | . . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘𝐴) ·ih 𝐵) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵)) | 
| 3 |  | fvoveq1 7454 | . . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝑇‘(𝐴 +ℎ 𝐵)) = (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))) | 
| 4 |  | oveq1 7438 | . . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 +ℎ 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) | 
| 5 | 3, 4 | oveq12d 7449 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) = ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))) | 
| 6 |  | fvoveq1 7454 | . . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝑇‘(𝐴 −ℎ 𝐵)) = (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) | 
| 7 |  | oveq1 7438 | . . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 −ℎ
𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) | 
| 8 | 6, 7 | oveq12d 7449 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵)) = ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) | 
| 9 | 5, 8 | oveq12d 7449 | . . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) = (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)))) | 
| 10 |  | fvoveq1 7454 | . . . . . . . 8
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) = (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵)))) | 
| 11 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 +ℎ (i
·ℎ 𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) | 
| 12 | 10, 11 | oveq12d 7449 | . . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) = ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵)))) | 
| 13 |  | fvoveq1 7454 | . . . . . . . 8
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) = (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))) | 
| 14 |  | oveq1 7438 | . . . . . . . 8
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 −ℎ (i
·ℎ 𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵))) | 
| 15 | 13, 14 | oveq12d 7449 | . . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))) = ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))) | 
| 16 | 12, 15 | oveq12d 7449 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))) = (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵))))) | 
| 17 | 16 | oveq2d 7447 | . . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (i ·
(((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))))) = (i · (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))))) | 
| 18 | 9, 17 | oveq12d 7449 | . . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) = ((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) + (i · (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵))))))) | 
| 19 | 18 | oveq1d 7446 | . . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) / 4) = (((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) + (i · (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))))) / 4)) | 
| 20 | 2, 19 | eqeq12d 2753 | . 2
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) / 4) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) = (((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) + (i · (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))))) / 4))) | 
| 21 |  | oveq2 7439 | . . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) | 
| 22 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ 𝐵) =
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ if(𝐵
∈ ℋ, 𝐵,
0ℎ))) | 
| 23 | 22 | fveq2d 6910 | . . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) = (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))) | 
| 24 | 23, 22 | oveq12d 7449 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) = ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))) | 
| 25 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) | 
| 26 | 25 | fveq2d 6910 | . . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) = (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) | 
| 27 | 26, 25 | oveq12d 7449 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) = ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) | 
| 28 | 24, 27 | oveq12d 7449 | . . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) = (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
− ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) | 
| 29 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (i
·ℎ 𝐵) = (i ·ℎ
if(𝐵 ∈ ℋ, 𝐵,
0ℎ))) | 
| 30 | 29 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) | 
| 31 | 30 | fveq2d 6910 | . . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) = (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) | 
| 32 | 31, 30 | oveq12d 7449 | . . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) = ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) | 
| 33 | 29 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))) | 
| 34 | 33 | fveq2d 6910 | . . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵))) = (𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))) | 
| 35 | 34, 33 | oveq12d 7449 | . . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵))) = ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))) | 
| 36 | 32, 35 | oveq12d 7449 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))) = (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))))) | 
| 37 | 36 | oveq2d 7447 | . . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (i ·
(((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵))))) = (i · (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))))))) | 
| 38 | 28, 37 | oveq12d 7449 | . . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) + (i · (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))))) = ((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
− ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) + (i ·
(((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ)))))))) | 
| 39 | 38 | oveq1d 7446 | . . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) + (i · (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))))) / 4) = (((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
− ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) + (i ·
(((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))))) /
4)) | 
| 40 | 21, 39 | eqeq12d 2753 | . 2
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) = (((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
𝐵)) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵)) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ 𝐵))) + (i · (((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ 𝐵))) ·ih
(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ 𝐵))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ 𝐵)))))) / 4) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
− ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) + (i ·
(((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))))) /
4))) | 
| 41 |  | lnopeq0.1 | . . 3
⊢ 𝑇 ∈ LinOp | 
| 42 |  | ifhvhv0 31041 | . . 3
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈
ℋ | 
| 43 |  | ifhvhv0 31041 | . . 3
⊢ if(𝐵 ∈ ℋ, 𝐵, 0ℎ) ∈
ℋ | 
| 44 | 41, 42, 43 | lnopeq0lem1 32024 | . 2
⊢ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (((((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
− ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) + (i ·
(((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
+ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ) +ℎ
(i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) − ((𝑇‘(if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))
·ih (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
−ℎ (i ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))))) /
4) | 
| 45 | 20, 40, 44 | dedth2h 4585 | 1
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) / 4)) |