Step | Hyp | Ref
| Expression |
1 | | ocval 30528 |
. . . 4
โข (๐ด โ โ โ
(โฅโ๐ด) = {๐ฅ โ โ โฃ
โ๐ฆ โ ๐ด (๐ฅ ยทih ๐ฆ) = 0}) |
2 | | ssrab2 4077 |
. . . 4
โข {๐ฅ โ โ โฃ
โ๐ฆ โ ๐ด (๐ฅ ยทih ๐ฆ) = 0} โ
โ |
3 | 1, 2 | eqsstrdi 4036 |
. . 3
โข (๐ด โ โ โ
(โฅโ๐ด) โ
โ) |
4 | | ssel 3975 |
. . . . . . 7
โข (๐ด โ โ โ (๐ฆ โ ๐ด โ ๐ฆ โ โ)) |
5 | | hi01 30344 |
. . . . . . 7
โข (๐ฆ โ โ โ
(0โ ยทih ๐ฆ) = 0) |
6 | 4, 5 | syl6 35 |
. . . . . 6
โข (๐ด โ โ โ (๐ฆ โ ๐ด โ (0โ
ยทih ๐ฆ) = 0)) |
7 | 6 | ralrimiv 3145 |
. . . . 5
โข (๐ด โ โ โ
โ๐ฆ โ ๐ด (0โ
ยทih ๐ฆ) = 0) |
8 | | ax-hv0cl 30251 |
. . . . 5
โข
0โ โ โ |
9 | 7, 8 | jctil 520 |
. . . 4
โข (๐ด โ โ โ
(0โ โ โ โง โ๐ฆ โ ๐ด (0โ
ยทih ๐ฆ) = 0)) |
10 | | ocel 30529 |
. . . 4
โข (๐ด โ โ โ
(0โ โ (โฅโ๐ด) โ (0โ โ
โ โง โ๐ฆ
โ ๐ด
(0โ ยทih ๐ฆ) = 0))) |
11 | 9, 10 | mpbird 256 |
. . 3
โข (๐ด โ โ โ
0โ โ (โฅโ๐ด)) |
12 | 3, 11 | jca 512 |
. 2
โข (๐ด โ โ โ
((โฅโ๐ด) โ
โ โง 0โ โ (โฅโ๐ด))) |
13 | | ssel2 3977 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ง โ ๐ด) โ ๐ง โ โ) |
14 | | ax-his2 30331 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = ((๐ฅ ยทih ๐ง) + (๐ฆ ยทih ๐ง))) |
15 | 14 | 3expa 1118 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = ((๐ฅ ยทih ๐ง) + (๐ฆ ยทih ๐ง))) |
16 | | oveq12 7417 |
. . . . . . . . . . . . . 14
โข (((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ
ยทih ๐ง) + (๐ฆ ยทih ๐ง)) = (0 + 0)) |
17 | | 00id 11388 |
. . . . . . . . . . . . . 14
โข (0 + 0) =
0 |
18 | 16, 17 | eqtrdi 2788 |
. . . . . . . . . . . . 13
โข (((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ
ยทih ๐ง) + (๐ฆ ยทih ๐ง)) = 0) |
19 | 15, 18 | sylan9eq 2792 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โง ((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0) |
20 | 19 | ex 413 |
. . . . . . . . . . 11
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0)) |
21 | 20 | ancoms 459 |
. . . . . . . . . 10
โข ((๐ง โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0)) |
22 | 13, 21 | sylan 580 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ง โ ๐ด) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (((๐ฅ
ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0)) |
23 | 22 | an32s 650 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ ๐ด) โ (((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ)
ยทih ๐ง) = 0)) |
24 | 23 | ralimdva 3167 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0) โ โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0)) |
25 | 24 | imdistanda 572 |
. . . . . 6
โข (๐ด โ โ โ (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0))) |
26 | | hvaddcl 30260 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ +โ ๐ฆ) โ
โ) |
27 | 26 | anim1i 615 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0) โ ((๐ฅ +โ ๐ฆ) โ โ โง
โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0)) |
28 | 25, 27 | syl6 35 |
. . . . 5
โข (๐ด โ โ โ (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ +โ ๐ฆ) โ โ โง
โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0))) |
29 | | ocel 30529 |
. . . . . . 7
โข (๐ด โ โ โ (๐ฅ โ (โฅโ๐ด) โ (๐ฅ โ โ โง โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0))) |
30 | | ocel 30529 |
. . . . . . 7
โข (๐ด โ โ โ (๐ฆ โ (โฅโ๐ด) โ (๐ฆ โ โ โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0))) |
31 | 29, 30 | anbi12d 631 |
. . . . . 6
โข (๐ด โ โ โ ((๐ฅ โ (โฅโ๐ด) โง ๐ฆ โ (โฅโ๐ด)) โ ((๐ฅ โ โ โง โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0) โง (๐ฆ โ โ โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0)))) |
32 | | an4 654 |
. . . . . . 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 623 |
. . . . . . 7
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง
(โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0 โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0))) |
35 | 32, 34 | bitr4i 277 |
. . . . . 6
โข (((๐ฅ โ โ โง
โ๐ง โ ๐ด (๐ฅ ยทih ๐ง) = 0) โง (๐ฆ โ โ โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0))) |
36 | 31, 35 | bitrdi 286 |
. . . . 5
โข (๐ด โ โ โ ((๐ฅ โ (โฅโ๐ด) โง ๐ฆ โ (โฅโ๐ด)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง โ๐ง โ ๐ด ((๐ฅ ยทih ๐ง) = 0 โง (๐ฆ ยทih ๐ง) = 0)))) |
37 | | ocel 30529 |
. . . . 5
โข (๐ด โ โ โ ((๐ฅ +โ ๐ฆ) โ (โฅโ๐ด) โ ((๐ฅ +โ ๐ฆ) โ โ โง โ๐ง โ ๐ด ((๐ฅ +โ ๐ฆ) ยทih ๐ง) = 0))) |
38 | 28, 36, 37 | 3imtr4d 293 |
. . . 4
โข (๐ด โ โ โ ((๐ฅ โ (โฅโ๐ด) โง ๐ฆ โ (โฅโ๐ด)) โ (๐ฅ +โ ๐ฆ) โ (โฅโ๐ด))) |
39 | 38 | ralrimivv 3198 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ
(โฅโ๐ด)โ๐ฆ โ (โฅโ๐ด)(๐ฅ +โ ๐ฆ) โ (โฅโ๐ด)) |
40 | | mul01 11392 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ (๐ฅ ยท 0) =
0) |
41 | | oveq2 7416 |
. . . . . . . . . . . . . 14
โข ((๐ฆ
ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = (๐ฅ ยท 0)) |
42 | 41 | eqeq1d 2734 |
. . . . . . . . . . . . 13
โข ((๐ฆ
ยทih ๐ง) = 0 โ ((๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0 โ (๐ฅ ยท 0) =
0)) |
43 | 40, 42 | syl5ibrcom 246 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ ((๐ฆ
ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
44 | 43 | ad2antrl 726 |
. . . . . . . . . . 11
โข ((๐ง โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฆ
ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
45 | | ax-his3 30332 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = (๐ฅ ยท (๐ฆ ยทih ๐ง))) |
46 | 45 | eqeq1d 2734 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ (((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
47 | 46 | 3expa 1118 |
. . . . . . . . . . . 12
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
48 | 47 | ancoms 459 |
. . . . . . . . . . 11
โข ((๐ง โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0 โ (๐ฅ ยท (๐ฆ ยทih ๐ง)) = 0)) |
49 | 44, 48 | sylibrd 258 |
. . . . . . . . . 10
โข ((๐ง โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฆ
ยทih ๐ง) = 0 โ ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0)) |
50 | 13, 49 | sylan 580 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ง โ ๐ด) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ฆ ยทih ๐ง) = 0 โ ((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0)) |
51 | 50 | an32s 650 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ ๐ด) โ ((๐ฆ ยทih ๐ง) = 0 โ ((๐ฅ
ยทโ ๐ฆ) ยทih ๐ง) = 0)) |
52 | 51 | ralimdva 3167 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0 โ โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0)) |
53 | 52 | imdistanda 572 |
. . . . . 6
โข (๐ด โ โ โ (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0))) |
54 | | hvmulcl 30261 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ ๐ฆ) โ โ) |
55 | 54 | anim1i 615 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0) โ ((๐ฅ ยทโ ๐ฆ) โ โ โง
โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0)) |
56 | 53, 55 | syl6 35 |
. . . . 5
โข (๐ด โ โ โ (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0) โ ((๐ฅ
ยทโ ๐ฆ) โ โ โง โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0))) |
57 | 30 | anbi2d 629 |
. . . . . 6
โข (๐ด โ โ โ ((๐ฅ โ โ โง ๐ฆ โ (โฅโ๐ด)) โ (๐ฅ โ โ โง (๐ฆ โ โ โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0)))) |
58 | | anass 469 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง
โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0) โ (๐ฅ โ โ โง (๐ฆ โ โ โง
โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0))) |
59 | 57, 58 | bitr4di 288 |
. . . . 5
โข (๐ด โ โ โ ((๐ฅ โ โ โง ๐ฆ โ (โฅโ๐ด)) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โง โ๐ง โ ๐ด (๐ฆ ยทih ๐ง) = 0))) |
60 | | ocel 30529 |
. . . . 5
โข (๐ด โ โ โ ((๐ฅ
ยทโ ๐ฆ) โ (โฅโ๐ด) โ ((๐ฅ ยทโ ๐ฆ) โ โ โง
โ๐ง โ ๐ด ((๐ฅ ยทโ ๐ฆ)
ยทih ๐ง) = 0))) |
61 | 56, 59, 60 | 3imtr4d 293 |
. . . 4
โข (๐ด โ โ โ ((๐ฅ โ โ โง ๐ฆ โ (โฅโ๐ด)) โ (๐ฅ ยทโ ๐ฆ) โ (โฅโ๐ด))) |
62 | 61 | ralrimivv 3198 |
. . 3
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ
(โฅโ๐ด)(๐ฅ
ยทโ ๐ฆ) โ (โฅโ๐ด)) |
63 | 39, 62 | jca 512 |
. 2
โข (๐ด โ โ โ
(โ๐ฅ โ
(โฅโ๐ด)โ๐ฆ โ (โฅโ๐ด)(๐ฅ +โ ๐ฆ) โ (โฅโ๐ด) โง โ๐ฅ โ โ โ๐ฆ โ (โฅโ๐ด)(๐ฅ ยทโ ๐ฆ) โ (โฅโ๐ด))) |
64 | | issh2 30457 |
. 2
โข
((โฅโ๐ด)
โ Sโ โ (((โฅโ๐ด) โ โ โง
0โ โ (โฅโ๐ด)) โง (โ๐ฅ โ (โฅโ๐ด)โ๐ฆ โ (โฅโ๐ด)(๐ฅ +โ ๐ฆ) โ (โฅโ๐ด) โง โ๐ฅ โ โ โ๐ฆ โ (โฅโ๐ด)(๐ฅ ยทโ ๐ฆ) โ (โฅโ๐ด)))) |
65 | 12, 63, 64 | sylanbrc 583 |
1
โข (๐ด โ โ โ
(โฅโ๐ด) โ
Sโ ) |