Proof of Theorem lnopeq0lem1
Step | Hyp | Ref
| Expression |
1 | | lnopeq0lem1.2 |
. . . 4
⊢ 𝐴 ∈ ℋ |
2 | | lnopeq0.1 |
. . . . . 6
⊢ 𝑇 ∈ LinOp |
3 | 2 | lnopfi 30050 |
. . . . 5
⊢ 𝑇: ℋ⟶
ℋ |
4 | 3 | ffvelrni 6903 |
. . . 4
⊢ (𝐴 ∈ ℋ → (𝑇‘𝐴) ∈ ℋ) |
5 | 1, 4 | ax-mp 5 |
. . 3
⊢ (𝑇‘𝐴) ∈ ℋ |
6 | | lnopeq0lem1.3 |
. . 3
⊢ 𝐵 ∈ ℋ |
7 | 3 | ffvelrni 6903 |
. . . 4
⊢ (𝐵 ∈ ℋ → (𝑇‘𝐵) ∈ ℋ) |
8 | 6, 7 | ax-mp 5 |
. . 3
⊢ (𝑇‘𝐵) ∈ ℋ |
9 | 5, 6, 8, 1 | polid2i 29238 |
. 2
⊢ ((𝑇‘𝐴) ·ih 𝐵) = ((((((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − (((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) ·ih
(𝐴
−ℎ 𝐵))) + (i · ((((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) / 4) |
10 | 2 | lnopaddi 30052 |
. . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵))) |
11 | 1, 6, 10 | mp2an 692 |
. . . . . 6
⊢ (𝑇‘(𝐴 +ℎ 𝐵)) = ((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) |
12 | 11 | oveq1i 7223 |
. . . . 5
⊢ ((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) = (((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) ·ih
(𝐴 +ℎ
𝐵)) |
13 | 2 | lnopsubi 30055 |
. . . . . . 7
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵))) |
14 | 1, 6, 13 | mp2an 692 |
. . . . . 6
⊢ (𝑇‘(𝐴 −ℎ 𝐵)) = ((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) |
15 | 14 | oveq1i 7223 |
. . . . 5
⊢ ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵)) = (((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) ·ih
(𝐴
−ℎ 𝐵)) |
16 | 12, 15 | oveq12i 7225 |
. . . 4
⊢ (((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) = ((((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − (((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) ·ih
(𝐴
−ℎ 𝐵))) |
17 | | ax-icn 10788 |
. . . . . . . 8
⊢ i ∈
ℂ |
18 | 2 | lnopaddmuli 30054 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℋ ∧ 𝐵
∈ ℋ) → (𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) = ((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵)))) |
19 | 17, 1, 6, 18 | mp3an 1463 |
. . . . . . 7
⊢ (𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) = ((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) |
20 | 19 | oveq1i 7223 |
. . . . . 6
⊢ ((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) = (((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) |
21 | 2 | lnopsubmuli 30056 |
. . . . . . . 8
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℋ ∧ 𝐵
∈ ℋ) → (𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) = ((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵)))) |
22 | 17, 1, 6, 21 | mp3an 1463 |
. . . . . . 7
⊢ (𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) = ((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) |
23 | 22 | oveq1i 7223 |
. . . . . 6
⊢ ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))) = (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))) |
24 | 20, 23 | oveq12i 7225 |
. . . . 5
⊢ (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))) = ((((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))) |
25 | 24 | oveq2i 7224 |
. . . 4
⊢ (i
· (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))))) = (i · ((((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵))))) |
26 | 16, 25 | oveq12i 7225 |
. . 3
⊢ ((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) = (((((𝑇‘𝐴) +ℎ (𝑇‘𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − (((𝑇‘𝐴) −ℎ (𝑇‘𝐵)) ·ih
(𝐴
−ℎ 𝐵))) + (i · ((((𝑇‘𝐴) +ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − (((𝑇‘𝐴) −ℎ (i
·ℎ (𝑇‘𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) |
27 | 26 | oveq1i 7223 |
. 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 2768 |
1
⊢ ((𝑇‘𝐴) ·ih 𝐵) = (((((𝑇‘(𝐴 +ℎ 𝐵)) ·ih
(𝐴 +ℎ
𝐵)) − ((𝑇‘(𝐴 −ℎ 𝐵))
·ih (𝐴 −ℎ 𝐵))) + (i · (((𝑇‘(𝐴 +ℎ (i
·ℎ 𝐵))) ·ih
(𝐴 +ℎ (i
·ℎ 𝐵))) − ((𝑇‘(𝐴 −ℎ (i
·ℎ 𝐵))) ·ih
(𝐴
−ℎ (i ·ℎ 𝐵)))))) / 4) |