Step | Hyp | Ref
| Expression |
1 | | ocval 30271 |
. . . 4
โข (๐ด โ โ โ
(โฅโ๐ด) = {๐ฅ โ โ โฃ
โ๐ฆ โ ๐ด (๐ฅ ยทih ๐ฆ) = 0}) |
2 | | ssrab2 4041 |
. . . 4
โข {๐ฅ โ โ โฃ
โ๐ฆ โ ๐ด (๐ฅ ยทih ๐ฆ) = 0} โ
โ |
3 | 1, 2 | eqsstrdi 4002 |
. . 3
โข (๐ด โ โ โ
(โฅโ๐ด) โ
โ) |
4 | | ssel 3941 |
. . . . . . 7
โข (๐ด โ โ โ (๐ฆ โ ๐ด โ ๐ฆ โ โ)) |
5 | | hi01 30087 |
. . . . . . 7
โข (๐ฆ โ โ โ
(0โ ยทih ๐ฆ) = 0) |
6 | 4, 5 | syl6 35 |
. . . . . 6
โข (๐ด โ โ โ (๐ฆ โ ๐ด โ (0โ
ยทih ๐ฆ) = 0)) |
7 | 6 | ralrimiv 3139 |
. . . . 5
โข (๐ด โ โ โ
โ๐ฆ โ ๐ด (0โ
ยทih ๐ฆ) = 0) |
8 | | ax-hv0cl 29994 |
. . . . 5
โข
0โ โ โ |
9 | 7, 8 | jctil 521 |
. . . 4
โข (๐ด โ โ โ
(0โ โ โ โง โ๐ฆ โ ๐ด (0โ
ยทih ๐ฆ) = 0)) |
10 | | ocel 30272 |
. . . 4
โข (๐ด โ โ โ
(0โ โ (โฅโ๐ด) โ (0โ โ
โ โง โ๐ฆ
โ ๐ด
(0โ ยทih ๐ฆ) = 0))) |
11 | 9, 10 | mpbird 257 |
. . 3
โข (๐ด โ โ โ
0โ โ (โฅโ๐ด)) |
12 | 3, 11 | jca 513 |
. 2
โข (๐ด โ โ โ
((โฅโ๐ด) โ
โ โง 0โ โ (โฅโ๐ด))) |
13 | | ssel2 3943 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ง โ ๐ด) โ ๐ง โ โ) |
14 | | ax-his2 30074 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = ((๐ฅ ยทih ๐ง) + (๐ฆ ยทih ๐ง))) |
15 | 14 | 3expa 1119 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = ((๐ฅ ยทih ๐ง) + (๐ฆ ยทih ๐ง))) |
16 | | oveq12 7370 |
. . . . . . . . . . . . . 14
โข (((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ
ยทih ๐ง) + (๐ฆ ยทih ๐ง)) = (0 + 0)) |
17 | | 00id 11338 |
. . . . . . . . . . . . . 14
โข (0 + 0) =
0 |
18 | 16, 17 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ
ยทih ๐ง) + (๐ฆ ยทih ๐ง)) = 0) |
19 | 15, 18 | sylan9eq 2793 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โง ((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0) |
20 | 19 | ex 414 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0)) |
21 | 20 | ancoms 460 |
. . . . . . . . . 10
โข ((๐ง โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0)) |
22 | 13, 21 | sylan 581 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ง โ ๐ด) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0)) |
23 | 22 | an32s 651 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ ๐ด) โ (((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0)) |
24 | 23 | ralimdva 3161 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0)) |
25 | 24 | imdistanda 573 |
. . . . . 6
โข (๐ด โ โ โ (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0))) |
26 | | hvaddcl 30003 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ +โ ๐ฆ) โ
โ) |
27 | 26 | anim1i 616 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ) โ โ โง
โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0)) |
28 | 25, 27 | syl6 35 |
. . . . 5
โข (๐ด โ โ โ (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ +โ ๐ฆ) โ โ โง
โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0))) |
29 | | ocel 30272 |
. . . . . . 7
โข (๐ด โ โ โ (๐ฅ โ (โฅโ๐ด) โ (๐ฅ โ โ โง โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0))) |
30 | | ocel 30272 |
. . . . . . 7
โข (๐ด โ โ โ (๐ฆ โ (โฅโ๐ด) โ (๐ฆ โ โ โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0))) |
31 | 29, 30 | anbi12d 632 |
. . . . . 6
โข (๐ด โ โ โ ((๐ฅ โ (โฅโ๐ด) โง ๐ฆ โ (โฅโ๐ด)) โ ((๐ฅ โ โ โง โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0) โง (๐ฆ โ โ โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0)))) |
32 | | an4 655 |
. . . . . . 7
โข (((๐ฅ โ โ โง
โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0) โง (๐ฆ โ โ โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง
(โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0 โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0))) |
33 | | r19.26 3111 |
. . . . . . . 8
โข
(โ๐ง โ
๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ (โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0 โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0)) |
34 | 33 | anbi2i 624 |
. . . . . . 7
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง
(โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0 โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0))) |
35 | 32, 34 | bitr4i 278 |
. . . . . 6
โข (((๐ฅ โ โ โง
โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0) โง (๐ฆ โ โ โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0))) |
36 | 31, 35 | bitrdi 287 |
. . . . 5
โข (๐ด โ โ โ ((๐ฅ โ (โฅโ๐ด) โง ๐ฆ โ (โฅโ๐ด)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)))) |
37 | | ocel 30272 |
. . . . 5
โข (๐ด โ โ โ ((๐ฅ +โ ๐ฆ) โ (โฅโ๐ด) โ ((๐ฅ +โ ๐ฆ) โ โ โง โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0))) |
38 | 28, 36, 37 | 3imtr4d 294 |
. . . 4
โข (๐ด โ โ โ ((๐ฅ โ (โฅโ๐ด) โง ๐ฆ โ (โฅโ๐ด)) โ (๐ฅ +โ ๐ฆ) โ (โฅโ๐ด))) |
39 | 38 | ralrimivv 3192 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ
(โฅโ๐ด)โ๐ฆ โ (โฅโ๐ด)(๐ฅ +โ ๐ฆ) โ (โฅโ๐ด)) |
40 | | mul01 11342 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ (๐ฅ ยท 0) =
0) |
41 | | oveq2 7369 |
. . . . . . . . . . . . . 14
โข ((๐ฆ
ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = (๐ฅ ยท 0)) |
42 | 41 | eqeq1d 2735 |
. . . . . . . . . . . . 13
โข ((๐ฆ
ยทih ๐ง) = 0 โ ((๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0 โ (๐ฅ ยท 0) =
0)) |
43 | 40, 42 | syl5ibrcom 247 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ ((๐ฆ
ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
44 | 43 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((๐ง โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฆ
ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
45 | | ax-his3 30075 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = (๐ฅ ยท (๐ฆ ยทih ๐ง))) |
46 | 45 | eqeq1d 2735 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ (((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
47 | 46 | 3expa 1119 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
48 | 47 | ancoms 460 |
. . . . . . . . . . 11
โข ((๐ง โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
49 | 44, 48 | sylibrd 259 |
. . . . . . . . . 10
โข ((๐ง โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฆ
ยทih ๐ง) = 0 โ ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0)) |
50 | 13, 49 | sylan 581 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ง โ ๐ด) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฆ ยทih ๐ง) = 0 โ ((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0)) |
51 | 50 | an32s 651 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ ๐ด) โ ((๐ฆ ยทih ๐ง) = 0 โ ((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0)) |
52 | 51 | ralimdva 3161 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0 โ โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0)) |
53 | 52 | imdistanda 573 |
. . . . . 6
โข (๐ด โ โ โ (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0))) |
54 | | hvmulcl 30004 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ ๐ฆ) โ โ) |
55 | 54 | anim1i 616 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0) โ ((๐ฅ ยทโ ๐ฆ) โ โ โง
โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0)) |
56 | 53, 55 | syl6 35 |
. . . . 5
โข (๐ด โ โ โ (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ
ยทโ ๐ฆ) โ โ โง โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0))) |
57 | 30 | anbi2d 630 |
. . . . . 6
โข (๐ด โ โ โ ((๐ฅ โ โ โง ๐ฆ โ (โฅโ๐ด)) โ (๐ฅ โ โ โง (๐ฆ โ โ โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0)))) |
58 | | anass 470 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0) โ (๐ฅ โ โ โง (๐ฆ โ โ โง
โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0))) |
59 | 57, 58 | bitr4di 289 |
. . . . 5
โข (๐ด โ โ โ ((๐ฅ โ โ โง ๐ฆ โ (โฅโ๐ด)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0))) |
60 | | ocel 30272 |
. . . . 5
โข (๐ด โ โ โ ((๐ฅ
ยทโ ๐ฆ) โ (โฅโ๐ด) โ ((๐ฅ ยทโ ๐ฆ) โ โ โง
โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0))) |
61 | 56, 59, 60 | 3imtr4d 294 |
. . . 4
โข (๐ด โ โ โ ((๐ฅ โ โ โง ๐ฆ โ (โฅโ๐ด)) โ (๐ฅ ยทโ ๐ฆ) โ (โฅโ๐ด))) |
62 | 61 | ralrimivv 3192 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ
(โฅโ๐ด)(๐ฅ
ยทโ ๐ฆ) โ (โฅโ๐ด)) |
63 | 39, 62 | jca 513 |
. 2
โข (๐ด โ โ โ
(โ๐ฅ โ
(โฅโ๐ด)โ๐ฆ โ (โฅโ๐ด)(๐ฅ +โ ๐ฆ) โ (โฅโ๐ด) โง โ๐ฅ โ โ โ๐ฆ โ (โฅโ๐ด)(๐ฅ ยทโ ๐ฆ) โ (โฅโ๐ด))) |
64 | | issh2 30200 |
. 2
โข
((โฅโ๐ด)
โ Sโ โ (((โฅโ๐ด) โ โ โง
0โ โ (โฅโ๐ด)) โง (โ๐ฅ โ (โฅโ๐ด)โ๐ฆ โ (โฅโ๐ด)(๐ฅ +โ ๐ฆ) โ (โฅโ๐ด) โง โ๐ฅ โ โ โ๐ฆ โ (โฅโ๐ด)(๐ฅ ยทโ ๐ฆ) โ (โฅโ๐ด)))) |
65 | 12, 63, 64 | sylanbrc 584 |
1
โข (๐ด โ โ โ
(โฅโ๐ด) โ
Sโ ) |