Step | Hyp | Ref
| Expression |
1 | | lnopeq0.1 |
. . . . . . 7
⊢ 𝑇 ∈ LinOp |
2 | 1 | lnopeq0lem2 30376 |
. . . . . 6
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑇‘𝑦) ·ih 𝑧) = (((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) / 4)) |
3 | 2 | adantl 482 |
. . . . 5
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘𝑦) ·ih 𝑧) = (((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) / 4)) |
4 | | hvaddcl 29382 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 +ℎ 𝑧) ∈
ℋ) |
5 | | fveq2 6766 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 +ℎ 𝑧) → (𝑇‘𝑥) = (𝑇‘(𝑦 +ℎ 𝑧))) |
6 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 +ℎ 𝑧) → 𝑥 = (𝑦 +ℎ 𝑧)) |
7 | 5, 6 | oveq12d 7285 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 +ℎ 𝑧) → ((𝑇‘𝑥) ·ih 𝑥) = ((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧))) |
8 | 7 | eqeq1d 2740 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 +ℎ 𝑧) → (((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ ((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) = 0)) |
9 | 8 | rspccva 3558 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 +ℎ 𝑧) ∈ ℋ) → ((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) = 0) |
10 | 4, 9 | sylan2 593 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) = 0) |
11 | | hvsubcl 29387 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 −ℎ
𝑧) ∈
ℋ) |
12 | | fveq2 6766 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 −ℎ 𝑧) → (𝑇‘𝑥) = (𝑇‘(𝑦 −ℎ 𝑧))) |
13 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 −ℎ 𝑧) → 𝑥 = (𝑦 −ℎ 𝑧)) |
14 | 12, 13 | oveq12d 7285 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑦 −ℎ 𝑧) → ((𝑇‘𝑥) ·ih 𝑥) = ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) |
15 | 14 | eqeq1d 2740 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 −ℎ 𝑧) → (((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧)) = 0)) |
16 | 15 | rspccva 3558 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 −ℎ 𝑧) ∈ ℋ) → ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧)) = 0) |
17 | 11, 16 | sylan2 593 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧)) = 0) |
18 | 10, 17 | oveq12d 7285 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) = (0 −
0)) |
19 | | 0m0e0 12103 |
. . . . . . . . . 10
⊢ (0
− 0) = 0 |
20 | 18, 19 | eqtrdi 2794 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) = 0) |
21 | | ax-icn 10940 |
. . . . . . . . . . . . . . . 16
⊢ i ∈
ℂ |
22 | | hvmulcl 29383 |
. . . . . . . . . . . . . . . 16
⊢ ((i
∈ ℂ ∧ 𝑧
∈ ℋ) → (i ·ℎ 𝑧) ∈ ℋ) |
23 | 21, 22 | mpan 687 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℋ → (i
·ℎ 𝑧) ∈ ℋ) |
24 | | hvaddcl 29382 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ (i
·ℎ 𝑧) ∈ ℋ) → (𝑦 +ℎ (i
·ℎ 𝑧)) ∈ ℋ) |
25 | 23, 24 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 +ℎ (i
·ℎ 𝑧)) ∈ ℋ) |
26 | | fveq2 6766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧)) → (𝑇‘𝑥) = (𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧)))) |
27 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧)) → 𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧))) |
28 | 26, 27 | oveq12d 7285 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧)) → ((𝑇‘𝑥) ·ih 𝑥) = ((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧)))) |
29 | 28 | eqeq1d 2740 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 +ℎ (i
·ℎ 𝑧)) → (((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ ((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) = 0)) |
30 | 29 | rspccva 3558 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 +ℎ (i
·ℎ 𝑧)) ∈ ℋ) → ((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) = 0) |
31 | 25, 30 | sylan2 593 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) = 0) |
32 | | hvsubcl 29387 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℋ ∧ (i
·ℎ 𝑧) ∈ ℋ) → (𝑦 −ℎ (i
·ℎ 𝑧)) ∈ ℋ) |
33 | 23, 32 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → (𝑦 −ℎ (i
·ℎ 𝑧)) ∈ ℋ) |
34 | | fveq2 6766 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧)) → (𝑇‘𝑥) = (𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧)))) |
35 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧)) → 𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧))) |
36 | 34, 35 | oveq12d 7285 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧)) → ((𝑇‘𝑥) ·ih 𝑥) = ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))) |
37 | 36 | eqeq1d 2740 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑦 −ℎ (i
·ℎ 𝑧)) → (((𝑇‘𝑥) ·ih 𝑥) = 0 ↔ ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))) = 0)) |
38 | 37 | rspccva 3558 |
. . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 −ℎ (i
·ℎ 𝑧)) ∈ ℋ) → ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))) = 0) |
39 | 33, 38 | sylan2 593 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))) = 0) |
40 | 31, 39 | oveq12d 7285 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))) = (0 −
0)) |
41 | 40, 19 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))) = 0) |
42 | 41 | oveq2d 7283 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))))) = (i ·
0)) |
43 | | it0e0 12205 |
. . . . . . . . . 10
⊢ (i
· 0) = 0 |
44 | 42, 43 | eqtrdi 2794 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧))))) = 0) |
45 | 20, 44 | oveq12d 7285 |
. . . . . . . 8
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) = (0 +
0)) |
46 | | 00id 11160 |
. . . . . . . 8
⊢ (0 + 0) =
0 |
47 | 45, 46 | eqtrdi 2794 |
. . . . . . 7
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) = 0) |
48 | 47 | oveq1d 7282 |
. . . . . 6
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) / 4) = (0 /
4)) |
49 | | 4cn 12068 |
. . . . . . 7
⊢ 4 ∈
ℂ |
50 | | 4ne0 12091 |
. . . . . . 7
⊢ 4 ≠
0 |
51 | 49, 50 | div0i 11719 |
. . . . . 6
⊢ (0 / 4) =
0 |
52 | 48, 51 | eqtrdi 2794 |
. . . . 5
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → (((((𝑇‘(𝑦 +ℎ 𝑧)) ·ih (𝑦 +ℎ 𝑧)) − ((𝑇‘(𝑦 −ℎ 𝑧))
·ih (𝑦 −ℎ 𝑧))) + (i · (((𝑇‘(𝑦 +ℎ (i
·ℎ 𝑧))) ·ih
(𝑦 +ℎ (i
·ℎ 𝑧))) − ((𝑇‘(𝑦 −ℎ (i
·ℎ 𝑧))) ·ih
(𝑦
−ℎ (i ·ℎ 𝑧)))))) / 4) =
0) |
53 | 3, 52 | eqtrd 2778 |
. . . 4
⊢
((∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ∧ (𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ)) → ((𝑇‘𝑦) ·ih 𝑧) = 0) |
54 | 53 | ralrimivva 3115 |
. . 3
⊢
(∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 → ∀𝑦 ∈ ℋ ∀𝑧 ∈ ℋ ((𝑇‘𝑦) ·ih 𝑧) = 0) |
55 | 1 | lnopfi 30339 |
. . . 4
⊢ 𝑇: ℋ⟶
ℋ |
56 | 55 | ho01i 30198 |
. . 3
⊢
(∀𝑦 ∈
ℋ ∀𝑧 ∈
ℋ ((𝑇‘𝑦)
·ih 𝑧) = 0 ↔ 𝑇 = 0hop ) |
57 | 54, 56 | sylib 217 |
. 2
⊢
(∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 → 𝑇 = 0hop ) |
58 | | fveq1 6765 |
. . . . . 6
⊢ (𝑇 = 0hop → (𝑇‘𝑥) = ( 0hop ‘𝑥)) |
59 | | ho0val 30120 |
. . . . . 6
⊢ (𝑥 ∈ ℋ → (
0hop ‘𝑥) =
0ℎ) |
60 | 58, 59 | sylan9eq 2798 |
. . . . 5
⊢ ((𝑇 = 0hop ∧ 𝑥 ∈ ℋ) → (𝑇‘𝑥) = 0ℎ) |
61 | 60 | oveq1d 7282 |
. . . 4
⊢ ((𝑇 = 0hop ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑥) ·ih 𝑥) = (0ℎ
·ih 𝑥)) |
62 | | hi01 29466 |
. . . . 5
⊢ (𝑥 ∈ ℋ →
(0ℎ ·ih 𝑥) = 0) |
63 | 62 | adantl 482 |
. . . 4
⊢ ((𝑇 = 0hop ∧ 𝑥 ∈ ℋ) →
(0ℎ ·ih 𝑥) = 0) |
64 | 61, 63 | eqtrd 2778 |
. . 3
⊢ ((𝑇 = 0hop ∧ 𝑥 ∈ ℋ) → ((𝑇‘𝑥) ·ih 𝑥) = 0) |
65 | 64 | ralrimiva 3108 |
. 2
⊢ (𝑇 = 0hop →
∀𝑥 ∈ ℋ
((𝑇‘𝑥)
·ih 𝑥) = 0) |
66 | 57, 65 | impbii 208 |
1
⊢
(∀𝑥 ∈
ℋ ((𝑇‘𝑥)
·ih 𝑥) = 0 ↔ 𝑇 = 0hop ) |