Step | Hyp | Ref
| Expression |
1 | | lnopeq0.1 |
. . . . . . 7
โข ๐ โ LinOp |
2 | 1 | lnopeq0lem2 30997 |
. . . . . 6
โข ((๐ฆ โ โ โง ๐ง โ โ) โ ((๐โ๐ฆ) ยทih ๐ง) = (((((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง))) + (i ยท (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง)))))) / 4)) |
3 | 2 | adantl 483 |
. . . . 5
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((๐โ๐ฆ) ยทih ๐ง) = (((((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง))) + (i ยท (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง)))))) / 4)) |
4 | | hvaddcl 30003 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ +โ ๐ง) โ
โ) |
5 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐ฆ +โ ๐ง) โ (๐โ๐ฅ) = (๐โ(๐ฆ +โ ๐ง))) |
6 | | id 22 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐ฆ +โ ๐ง) โ ๐ฅ = (๐ฆ +โ ๐ง)) |
7 | 5, 6 | oveq12d 7379 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (๐ฆ +โ ๐ง) โ ((๐โ๐ฅ) ยทih ๐ฅ) = ((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง))) |
8 | 7 | eqeq1d 2735 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ฆ +โ ๐ง) โ (((๐โ๐ฅ) ยทih ๐ฅ) = 0 โ ((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) = 0)) |
9 | 8 | rspccva 3582 |
. . . . . . . . . . . 12
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ +โ ๐ง) โ โ) โ ((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) = 0) |
10 | 4, 9 | sylan2 594 |
. . . . . . . . . . 11
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) = 0) |
11 | | hvsubcl 30008 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ โโ
๐ง) โ
โ) |
12 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐ฆ โโ ๐ง) โ (๐โ๐ฅ) = (๐โ(๐ฆ โโ ๐ง))) |
13 | | id 22 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐ฆ โโ ๐ง) โ ๐ฅ = (๐ฆ โโ ๐ง)) |
14 | 12, 13 | oveq12d 7379 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (๐ฆ โโ ๐ง) โ ((๐โ๐ฅ) ยทih ๐ฅ) = ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง))) |
15 | 14 | eqeq1d 2735 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ฆ โโ ๐ง) โ (((๐โ๐ฅ) ยทih ๐ฅ) = 0 โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง)) = 0)) |
16 | 15 | rspccva 3582 |
. . . . . . . . . . . 12
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โโ ๐ง) โ โ) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง)) = 0) |
17 | 11, 16 | sylan2 594 |
. . . . . . . . . . 11
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง)) = 0) |
18 | 10, 17 | oveq12d 7379 |
. . . . . . . . . 10
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ (((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง))) = (0 โ
0)) |
19 | | 0m0e0 12281 |
. . . . . . . . . 10
โข (0
โ 0) = 0 |
20 | 18, 19 | eqtrdi 2789 |
. . . . . . . . 9
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ (((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง))) = 0) |
21 | | ax-icn 11118 |
. . . . . . . . . . . . . . . 16
โข i โ
โ |
22 | | hvmulcl 30004 |
. . . . . . . . . . . . . . . 16
โข ((i
โ โ โง ๐ง
โ โ) โ (i ยทโ ๐ง) โ โ) |
23 | 21, 22 | mpan 689 |
. . . . . . . . . . . . . . 15
โข (๐ง โ โ โ (i
ยทโ ๐ง) โ โ) |
24 | | hvaddcl 30003 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ โง (i
ยทโ ๐ง) โ โ) โ (๐ฆ +โ (i
ยทโ ๐ง)) โ โ) |
25 | 23, 24 | sylan2 594 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ +โ (i
ยทโ ๐ง)) โ โ) |
26 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = (๐ฆ +โ (i
ยทโ ๐ง)) โ (๐โ๐ฅ) = (๐โ(๐ฆ +โ (i
ยทโ ๐ง)))) |
27 | | id 22 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = (๐ฆ +โ (i
ยทโ ๐ง)) โ ๐ฅ = (๐ฆ +โ (i
ยทโ ๐ง))) |
28 | 26, 27 | oveq12d 7379 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = (๐ฆ +โ (i
ยทโ ๐ง)) โ ((๐โ๐ฅ) ยทih ๐ฅ) = ((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง)))) |
29 | 28 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐ฆ +โ (i
ยทโ ๐ง)) โ (((๐โ๐ฅ) ยทih ๐ฅ) = 0 โ ((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) = 0)) |
30 | 29 | rspccva 3582 |
. . . . . . . . . . . . . 14
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ +โ (i
ยทโ ๐ง)) โ โ) โ ((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) = 0) |
31 | 25, 30 | sylan2 594 |
. . . . . . . . . . . . 13
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) = 0) |
32 | | hvsubcl 30008 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ โง (i
ยทโ ๐ง) โ โ) โ (๐ฆ โโ (i
ยทโ ๐ง)) โ โ) |
33 | 23, 32 | sylan2 594 |
. . . . . . . . . . . . . 14
โข ((๐ฆ โ โ โง ๐ง โ โ) โ (๐ฆ โโ (i
ยทโ ๐ง)) โ โ) |
34 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = (๐ฆ โโ (i
ยทโ ๐ง)) โ (๐โ๐ฅ) = (๐โ(๐ฆ โโ (i
ยทโ ๐ง)))) |
35 | | id 22 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = (๐ฆ โโ (i
ยทโ ๐ง)) โ ๐ฅ = (๐ฆ โโ (i
ยทโ ๐ง))) |
36 | 34, 35 | oveq12d 7379 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = (๐ฆ โโ (i
ยทโ ๐ง)) โ ((๐โ๐ฅ) ยทih ๐ฅ) = ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง)))) |
37 | 36 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐ฆ โโ (i
ยทโ ๐ง)) โ (((๐โ๐ฅ) ยทih ๐ฅ) = 0 โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง))) = 0)) |
38 | 37 | rspccva 3582 |
. . . . . . . . . . . . . 14
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โโ (i
ยทโ ๐ง)) โ โ) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง))) = 0) |
39 | 33, 38 | sylan2 594 |
. . . . . . . . . . . . 13
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง))) = 0) |
40 | 31, 39 | oveq12d 7379 |
. . . . . . . . . . . 12
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง)))) = (0 โ
0)) |
41 | 40, 19 | eqtrdi 2789 |
. . . . . . . . . . 11
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง)))) = 0) |
42 | 41 | oveq2d 7377 |
. . . . . . . . . 10
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ (i ยท (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง))))) = (i ยท
0)) |
43 | | it0e0 12383 |
. . . . . . . . . 10
โข (i
ยท 0) = 0 |
44 | 42, 43 | eqtrdi 2789 |
. . . . . . . . 9
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ (i ยท (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง))))) = 0) |
45 | 20, 44 | oveq12d 7379 |
. . . . . . . 8
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง))) + (i ยท (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง)))))) = (0 +
0)) |
46 | | 00id 11338 |
. . . . . . . 8
โข (0 + 0) =
0 |
47 | 45, 46 | eqtrdi 2789 |
. . . . . . 7
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง))) + (i ยท (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง)))))) = 0) |
48 | 47 | oveq1d 7376 |
. . . . . 6
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ (((((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง))) + (i ยท (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง)))))) / 4) = (0 /
4)) |
49 | | 4cn 12246 |
. . . . . . 7
โข 4 โ
โ |
50 | | 4ne0 12269 |
. . . . . . 7
โข 4 โ
0 |
51 | 49, 50 | div0i 11897 |
. . . . . 6
โข (0 / 4) =
0 |
52 | 48, 51 | eqtrdi 2789 |
. . . . 5
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ (((((๐โ(๐ฆ +โ ๐ง)) ยทih (๐ฆ +โ ๐ง)) โ ((๐โ(๐ฆ โโ ๐ง))
ยทih (๐ฆ โโ ๐ง))) + (i ยท (((๐โ(๐ฆ +โ (i
ยทโ ๐ง))) ยทih
(๐ฆ +โ (i
ยทโ ๐ง))) โ ((๐โ(๐ฆ โโ (i
ยทโ ๐ง))) ยทih
(๐ฆ
โโ (i ยทโ ๐ง)))))) / 4) =
0) |
53 | 3, 52 | eqtrd 2773 |
. . . 4
โข
((โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โง (๐ฆ โ โ โง ๐ง โ โ)) โ ((๐โ๐ฆ) ยทih ๐ง) = 0) |
54 | 53 | ralrimivva 3194 |
. . 3
โข
(โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โ โ๐ฆ โ โ โ๐ง โ โ ((๐โ๐ฆ) ยทih ๐ง) = 0) |
55 | 1 | lnopfi 30960 |
. . . 4
โข ๐: โโถ
โ |
56 | 55 | ho01i 30819 |
. . 3
โข
(โ๐ฆ โ
โ โ๐ง โ
โ ((๐โ๐ฆ)
ยทih ๐ง) = 0 โ ๐ = 0hop ) |
57 | 54, 56 | sylib 217 |
. 2
โข
(โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โ ๐ = 0hop ) |
58 | | fveq1 6845 |
. . . . . 6
โข (๐ = 0hop โ (๐โ๐ฅ) = ( 0hop โ๐ฅ)) |
59 | | ho0val 30741 |
. . . . . 6
โข (๐ฅ โ โ โ (
0hop โ๐ฅ) =
0โ) |
60 | 58, 59 | sylan9eq 2793 |
. . . . 5
โข ((๐ = 0hop โง ๐ฅ โ โ) โ (๐โ๐ฅ) = 0โ) |
61 | 60 | oveq1d 7376 |
. . . 4
โข ((๐ = 0hop โง ๐ฅ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) = (0โ
ยทih ๐ฅ)) |
62 | | hi01 30087 |
. . . . 5
โข (๐ฅ โ โ โ
(0โ ยทih ๐ฅ) = 0) |
63 | 62 | adantl 483 |
. . . 4
โข ((๐ = 0hop โง ๐ฅ โ โ) โ
(0โ ยทih ๐ฅ) = 0) |
64 | 61, 63 | eqtrd 2773 |
. . 3
โข ((๐ = 0hop โง ๐ฅ โ โ) โ ((๐โ๐ฅ) ยทih ๐ฅ) = 0) |
65 | 64 | ralrimiva 3140 |
. 2
โข (๐ = 0hop โ
โ๐ฅ โ โ
((๐โ๐ฅ)
ยทih ๐ฅ) = 0) |
66 | 57, 65 | impbii 208 |
1
โข
(โ๐ฅ โ
โ ((๐โ๐ฅ)
ยทih ๐ฅ) = 0 โ ๐ = 0hop ) |