| Step | Hyp | Ref
| Expression |
| 1 | | lnopeq0.1 |
. . . . . . 7
⊢ 𝑇 ∈ LinOp |
| 2 | 1 | lnopeq0lem2 32025 |
. . . . . 6
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑇‘𝑦) ·ih 𝑧) = (((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) / 4)) |
| 3 | 2 | adantl 481 |
. . . . 5
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘𝑦) ·ih 𝑧) = (((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) / 4)) |
| 4 | | hvaddcl 31031 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 +ℎ 𝑧) ∈
ℋ) |
| 5 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 +ℎ 𝑧) → (𝑇‘𝑥) = (𝑇‘(𝑦 +ℎ 𝑧))) |
| 6 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 = (𝑦 +ℎ 𝑧)) |
| 7 | 5, 6 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 +ℎ 𝑧) → ((𝑇‘𝑥) ·ih 𝑥) = ((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧))) |
| 8 | 7 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 +ℎ 𝑧) → (((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ ((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) = 0)) |
| 9 | 8 | rspccva 3621 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 +ℎ 𝑧) ∈ ℋ) → ((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) = 0) |
| 10 | 4, 9 | sylan2 593 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) = 0) |
| 11 | | hvsubcl 31036 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 −ℎ
𝑧) ∈
ℋ) |
| 12 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 −ℎ 𝑧) → (𝑇‘𝑥) = (𝑇‘(𝑦 −ℎ 𝑧))) |
| 13 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 −ℎ 𝑧) → 𝑥 = (𝑦 −ℎ 𝑧)) |
| 14 | 12, 13 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 −ℎ 𝑧) → ((𝑇‘𝑥) ·ih 𝑥) = ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) |
| 15 | 14 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 −ℎ 𝑧) → (((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧)) = 0)) |
| 16 | 15 | rspccva 3621 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 −ℎ 𝑧) ∈ ℋ) → ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧)) = 0) |
| 17 | 11, 16 | sylan2 593 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧)) = 0) |
| 18 | 10, 17 | oveq12d 7449 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) = (0 −
0)) |
| 19 | | 0m0e0 12386 |
. . . . . . . . . 10
⊢ (0
− 0) = 0 |
| 20 | 18, 19 | eqtrdi 2793 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) = 0) |
| 21 | | ax-icn 11214 |
. . . . . . . . . . . . . . . 16
⊢ i ∈
ℂ |
| 22 | | hvmulcl 31032 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ 𝑧
∈ ℋ) → (i ·ℎ 𝑧) ∈ ℋ) |
| 23 | 21, 22 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℋ → (i
·ℎ 𝑧) ∈ ℋ) |
| 24 | | hvaddcl 31031 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ (i
·ℎ 𝑧) ∈ ℋ) → (𝑦 +ℎ (i
·ℎ 𝑧)) ∈ ℋ) |
| 25 | 23, 24 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 +ℎ (i
·ℎ 𝑧)) ∈ ℋ) |
| 26 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧)) → (𝑇‘𝑥) = (𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧)))) |
| 27 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧)) → 𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧))) |
| 28 | 26, 27 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧)) → ((𝑇‘𝑥) ·ih 𝑥) = ((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧)))) |
| 29 | 28 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧)) → (((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ ((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) = 0)) |
| 30 | 29 | rspccva 3621 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 +ℎ (i
·ℎ 𝑧)) ∈ ℋ) → ((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) = 0) |
| 31 | 25, 30 | sylan2 593 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) = 0) |
| 32 | | hvsubcl 31036 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ (i
·ℎ 𝑧) ∈ ℋ) → (𝑦 −ℎ (i
·ℎ 𝑧)) ∈ ℋ) |
| 33 | 23, 32 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 −ℎ (i
·ℎ 𝑧)) ∈ ℋ) |
| 34 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧)) → (𝑇‘𝑥) = (𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧)))) |
| 35 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧)) → 𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧))) |
| 36 | 34, 35 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧)) → ((𝑇‘𝑥) ·ih 𝑥) = ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))) |
| 37 | 36 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧)) → (((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))) = 0)) |
| 38 | 37 | rspccva 3621 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 −ℎ (i
·ℎ 𝑧)) ∈ ℋ) → ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))) = 0) |
| 39 | 33, 38 | sylan2 593 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))) = 0) |
| 40 | 31, 39 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))) = (0 −
0)) |
| 41 | 40, 19 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))) = 0) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))))) = (i ·
0)) |
| 43 | | it0e0 12488 |
. . . . . . . . . 10
⊢ (i
· 0) = 0 |
| 44 | 42, 43 | eqtrdi 2793 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))))) = 0) |
| 45 | 20, 44 | oveq12d 7449 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) = (0 +
0)) |
| 46 | | 00id 11436 |
. . . . . . . 8
⊢ (0 + 0) =
0 |
| 47 | 45, 46 | eqtrdi 2793 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) = 0) |
| 48 | 47 | oveq1d 7446 |
. . . . . 6
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) / 4) = (0 /
4)) |
| 49 | | 4cn 12351 |
. . . . . . 7
⊢ 4 ∈
ℂ |
| 50 | | 4ne0 12374 |
. . . . . . 7
⊢ 4 ≠
0 |
| 51 | 49, 50 | div0i 12001 |
. . . . . 6
⊢ (0 / 4) =
0 |
| 52 | 48, 51 | eqtrdi 2793 |
. . . . 5
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) / 4) =
0) |
| 53 | 3, 52 | eqtrd 2777 |
. . . 4
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘𝑦) ·ih 𝑧) = 0) |
| 54 | 53 | ralrimivva 3202 |
. . 3
⊢
(∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 → ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ ((𝑇‘𝑦) ·ih 𝑧) = 0) |
| 55 | 1 | lnopfi 31988 |
. . . 4
⊢ 𝑇: ℋ⟶
ℋ |
| 56 | 55 | ho01i 31847 |
. . 3
⊢
(∀𝑦 ∈
ℋ ∀𝑧 ∈
ℋ ((𝑇‘𝑦)
·ih 𝑧) = 0 ↔ 𝑇 = 0hop ) |
| 57 | 54, 56 | sylib 218 |
. 2
⊢
(∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 → 𝑇 = 0hop ) |
| 58 | | fveq1 6905 |
. . . . . 6
⊢ (𝑇 = 0hop → (𝑇‘𝑥) = ( 0hop ‘𝑥)) |
| 59 | | ho0val 31769 |
. . . . . 6
⊢ (𝑥 ∈ ℋ → (
0hop ‘𝑥) =
0ℎ) |
| 60 | 58, 59 | sylan9eq 2797 |
. . . . 5
⊢ ((𝑇 = 0hop ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) = 0ℎ) |
| 61 | 60 | oveq1d 7446 |
. . . 4
⊢ ((𝑇 = 0hop ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑥) ·ih 𝑥) = (0ℎ
·ih 𝑥)) |
| 62 | | hi01 31115 |
. . . . 5
⊢ (𝑥 ∈ ℋ →
(0ℎ ·ih 𝑥) = 0) |
| 63 | 62 | adantl 481 |
. . . 4
⊢ ((𝑇 = 0hop ∧ 𝑥 ∈ ℋ) →
(0ℎ ·ih 𝑥) = 0) |
| 64 | 61, 63 | eqtrd 2777 |
. . 3
⊢ ((𝑇 = 0hop ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑥) ·ih 𝑥) = 0) |
| 65 | 64 | ralrimiva 3146 |
. 2
⊢ (𝑇 = 0hop →
∀𝑥 ∈ ℋ
((𝑇‘𝑥)
·ih 𝑥) = 0) |
| 66 | 57, 65 | impbii 209 |
1
⊢
(∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ↔ 𝑇 = 0hop ) |