Proof of Theorem lnopeq0lem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lnopeq0lem1.2 | . . . 4
⊢ 𝐴 ∈ ℋ | 
| 2 |  | lnopeq0.1 | . . . . . 6
⊢ 𝑇 ∈ LinOp | 
| 3 | 2 | lnopfi 31989 | . . . . 5
⊢ 𝑇: ℋ⟶
ℋ | 
| 4 | 3 | ffvelcdmi 7102 | . . . 4
⊢ (𝐴 ∈ ℋ → (𝑇‘𝐴) ∈ ℋ) | 
| 5 | 1, 4 | ax-mp 5 | . . 3
⊢ (𝑇‘𝐴) ∈ ℋ | 
| 6 |  | lnopeq0lem1.3 | . . 3
⊢ 𝐵 ∈ ℋ | 
| 7 | 3 | ffvelcdmi 7102 | . . . 4
⊢ (𝐵 ∈ ℋ → (𝑇‘𝐵) ∈ ℋ) | 
| 8 | 6, 7 | ax-mp 5 | . . 3
⊢ (𝑇‘𝐵) ∈ ℋ | 
| 9 | 5, 6, 8, 1 | polid2i 31177 | . 2
⊢ ((𝑇‘𝐴) ·ih 𝐵) = ((((((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − (((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) ·ih
(𝐴
−ℎ 𝐵))) + (i · ((((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) / 4) | 
| 10 | 2 | lnopaddi 31991 | . . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵))) | 
| 11 | 1, 6, 10 | mp2an 692 | . . . . . 6
⊢ (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) | 
| 12 | 11 | oveq1i 7442 | . . . . 5
⊢ ((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) = (((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) ·ih
(𝐴 +ℎ
𝐵)) | 
| 13 | 2 | lnopsubi 31994 | . . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵))) | 
| 14 | 1, 6, 13 | mp2an 692 | . . . . . 6
⊢ (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) | 
| 15 | 14 | oveq1i 7442 | . . . . 5
⊢ ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵)) = (((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) ·ih
(𝐴
−ℎ 𝐵)) | 
| 16 | 12, 15 | oveq12i 7444 | . . . 4
⊢ (((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) = ((((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − (((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) ·ih
(𝐴
−ℎ 𝐵))) | 
| 17 |  | ax-icn 11215 | . . . . . . . 8
⊢ i ∈
ℂ | 
| 18 | 2 | lnopaddmuli 31993 | . . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℋ ∧ 𝐵
∈ ℋ) → (𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) = ((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵)))) | 
| 19 | 17, 1, 6, 18 | mp3an 1462 | . . . . . . 7
⊢ (𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) = ((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) | 
| 20 | 19 | oveq1i 7442 | . . . . . 6
⊢ ((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) = (((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) | 
| 21 | 2 | lnopsubmuli 31995 | . . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℋ ∧ 𝐵
∈ ℋ) → (𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) = ((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵)))) | 
| 22 | 17, 1, 6, 21 | mp3an 1462 | . . . . . . 7
⊢ (𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) = ((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) | 
| 23 | 22 | oveq1i 7442 | . . . . . 6
⊢ ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))) = (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))) | 
| 24 | 20, 23 | oveq12i 7444 | . . . . 5
⊢ (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))) = ((((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))) | 
| 25 | 24 | oveq2i 7443 | . . . 4
⊢ (i
· (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))))) = (i · ((((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))))) | 
| 26 | 16, 25 | oveq12i 7444 | . . 3
⊢ ((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) = (((((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − (((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) ·ih
(𝐴
−ℎ 𝐵))) + (i · ((((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) | 
| 27 | 26 | oveq1i 7442 | . 2
⊢
(((((𝑇‘(𝐴 +ℎ 𝐵))
·ih (𝐴 +ℎ 𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) / 4) = ((((((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − (((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) ·ih
(𝐴
−ℎ 𝐵))) + (i · ((((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) / 4) | 
| 28 | 9, 27 | eqtr4i 2767 | 1
⊢ ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) / 4) |