Step | Hyp | Ref
| Expression |
1 | | pjco.2 |
. . . . . . 7
โข ๐ป โ
Cโ |
2 | | pjco.1 |
. . . . . . 7
โข ๐บ โ
Cโ |
3 | 1, 2 | pjssmi 31149 |
. . . . . 6
โข (๐ฅ โ โ โ (๐บ โ ๐ป โ
(((projโโ๐ป)โ๐ฅ) โโ
((projโโ๐บ)โ๐ฅ)) = ((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ))) |
4 | 1, 2 | pjssge0i 31150 |
. . . . . 6
โข (๐ฅ โ โ โ
((((projโโ๐ป)โ๐ฅ) โโ
((projโโ๐บ)โ๐ฅ)) = ((projโโ(๐ป โฉ (โฅโ๐บ)))โ๐ฅ) โ 0 โค
((((projโโ๐ป)โ๐ฅ) โโ
((projโโ๐บ)โ๐ฅ)) ยทih ๐ฅ))) |
5 | 3, 4 | syld 47 |
. . . . 5
โข (๐ฅ โ โ โ (๐บ โ ๐ป โ 0 โค
((((projโโ๐ป)โ๐ฅ) โโ
((projโโ๐บ)โ๐ฅ)) ยทih ๐ฅ))) |
6 | 1, 2 | pjdifnormi 31151 |
. . . . 5
โข (๐ฅ โ โ โ (0 โค
((((projโโ๐ป)โ๐ฅ) โโ
((projโโ๐บ)โ๐ฅ)) ยทih ๐ฅ) โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)))) |
7 | 5, 6 | sylibd 238 |
. . . 4
โข (๐ฅ โ โ โ (๐บ โ ๐ป โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)))) |
8 | 7 | com12 32 |
. . 3
โข (๐บ โ ๐ป โ (๐ฅ โ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)))) |
9 | 8 | ralrimiv 3139 |
. 2
โข (๐บ โ ๐ป โ โ๐ฅ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) |
10 | 1 | choccli 30291 |
. . . . . . . 8
โข
(โฅโ๐ป)
โ Cโ |
11 | 10 | cheli 30216 |
. . . . . . 7
โข (๐ฅ โ (โฅโ๐ป) โ ๐ฅ โ โ) |
12 | | breq2 5110 |
. . . . . . . . . . . . 13
โข
((normโโ((projโโ๐ป)โ๐ฅ)) = 0 โ
((normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)) โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค 0)) |
13 | 12 | biimpac 480 |
. . . . . . . . . . . 12
โข
(((normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)) โง
(normโโ((projโโ๐ป)โ๐ฅ)) = 0) โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค 0) |
14 | 2 | pjhcli 30402 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โ โ
((projโโ๐บ)โ๐ฅ) โ โ) |
15 | | normge0 30110 |
. . . . . . . . . . . . . . 15
โข
(((projโโ๐บ)โ๐ฅ) โ โ โ 0 โค
(normโโ((projโโ๐บ)โ๐ฅ))) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ 0 โค
(normโโ((projโโ๐บ)โ๐ฅ))) |
17 | | normcl 30109 |
. . . . . . . . . . . . . . . 16
โข
(((projโโ๐บ)โ๐ฅ) โ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โ โ) |
18 | 14, 17 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โ โ) |
19 | | 0re 11162 |
. . . . . . . . . . . . . . 15
โข 0 โ
โ |
20 | | letri3 11245 |
. . . . . . . . . . . . . . . 16
โข
(((normโโ((projโโ๐บ)โ๐ฅ)) โ โ โง 0 โ โ)
โ ((normโโ((projโโ๐บ)โ๐ฅ)) = 0 โ
((normโโ((projโโ๐บ)โ๐ฅ)) โค 0 โง 0 โค
(normโโ((projโโ๐บ)โ๐ฅ))))) |
21 | 20 | biimprd 248 |
. . . . . . . . . . . . . . 15
โข
(((normโโ((projโโ๐บ)โ๐ฅ)) โ โ โง 0 โ โ)
โ (((normโโ((projโโ๐บ)โ๐ฅ)) โค 0 โง 0 โค
(normโโ((projโโ๐บ)โ๐ฅ))) โ
(normโโ((projโโ๐บ)โ๐ฅ)) = 0)) |
22 | 18, 19, 21 | sylancl 587 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ
(((normโโ((projโโ๐บ)โ๐ฅ)) โค 0 โง 0 โค
(normโโ((projโโ๐บ)โ๐ฅ))) โ
(normโโ((projโโ๐บ)โ๐ฅ)) = 0)) |
23 | 16, 22 | sylan2i 607 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ
(((normโโ((projโโ๐บ)โ๐ฅ)) โค 0 โง ๐ฅ โ โ) โ
(normโโ((projโโ๐บ)โ๐ฅ)) = 0)) |
24 | 23 | anabsi6 669 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง
(normโโ((projโโ๐บ)โ๐ฅ)) โค 0) โ
(normโโ((projโโ๐บ)โ๐ฅ)) = 0) |
25 | 13, 24 | sylan2 594 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง
((normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)) โง
(normโโ((projโโ๐ป)โ๐ฅ)) = 0)) โ
(normโโ((projโโ๐บ)โ๐ฅ)) = 0) |
26 | 25 | expr 458 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) โ
((normโโ((projโโ๐ป)โ๐ฅ)) = 0 โ
(normโโ((projโโ๐บ)โ๐ฅ)) = 0)) |
27 | 1 | pjhcli 30402 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ
((projโโ๐ป)โ๐ฅ) โ โ) |
28 | | norm-i 30113 |
. . . . . . . . . . . . 13
โข
(((projโโ๐ป)โ๐ฅ) โ โ โ
((normโโ((projโโ๐ป)โ๐ฅ)) = 0 โ
((projโโ๐ป)โ๐ฅ) = 0โ)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
((normโโ((projโโ๐ป)โ๐ฅ)) = 0 โ
((projโโ๐ป)โ๐ฅ) = 0โ)) |
30 | | pjoc2 30423 |
. . . . . . . . . . . . 13
โข ((๐ป โ
Cโ โง ๐ฅ โ โ) โ (๐ฅ โ (โฅโ๐ป) โ
((projโโ๐ป)โ๐ฅ) = 0โ)) |
31 | 1, 30 | mpan 689 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ (๐ฅ โ (โฅโ๐ป) โ
((projโโ๐ป)โ๐ฅ) = 0โ)) |
32 | 29, 31 | bitr4d 282 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
((normโโ((projโโ๐ป)โ๐ฅ)) = 0 โ ๐ฅ โ (โฅโ๐ป))) |
33 | 32 | adantr 482 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) โ
((normโโ((projโโ๐ป)โ๐ฅ)) = 0 โ ๐ฅ โ (โฅโ๐ป))) |
34 | | norm-i 30113 |
. . . . . . . . . . . . 13
โข
(((projโโ๐บ)โ๐ฅ) โ โ โ
((normโโ((projโโ๐บ)โ๐ฅ)) = 0 โ
((projโโ๐บ)โ๐ฅ) = 0โ)) |
35 | 14, 34 | syl 17 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ
((normโโ((projโโ๐บ)โ๐ฅ)) = 0 โ
((projโโ๐บ)โ๐ฅ) = 0โ)) |
36 | | pjoc2 30423 |
. . . . . . . . . . . . 13
โข ((๐บ โ
Cโ โง ๐ฅ โ โ) โ (๐ฅ โ (โฅโ๐บ) โ
((projโโ๐บ)โ๐ฅ) = 0โ)) |
37 | 2, 36 | mpan 689 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ (๐ฅ โ (โฅโ๐บ) โ
((projโโ๐บ)โ๐ฅ) = 0โ)) |
38 | 35, 37 | bitr4d 282 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
((normโโ((projโโ๐บ)โ๐ฅ)) = 0 โ ๐ฅ โ (โฅโ๐บ))) |
39 | 38 | adantr 482 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) โ
((normโโ((projโโ๐บ)โ๐ฅ)) = 0 โ ๐ฅ โ (โฅโ๐บ))) |
40 | 26, 33, 39 | 3imtr3d 293 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) โ (๐ฅ โ (โฅโ๐ป) โ ๐ฅ โ (โฅโ๐บ))) |
41 | 40 | ex 414 |
. . . . . . . 8
โข (๐ฅ โ โ โ
((normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)) โ (๐ฅ โ (โฅโ๐ป) โ ๐ฅ โ (โฅโ๐บ)))) |
42 | 41 | a2i 14 |
. . . . . . 7
โข ((๐ฅ โ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) โ (๐ฅ โ โ โ (๐ฅ โ (โฅโ๐ป) โ ๐ฅ โ (โฅโ๐บ)))) |
43 | 11, 42 | syl5 34 |
. . . . . 6
โข ((๐ฅ โ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) โ (๐ฅ โ (โฅโ๐ป) โ (๐ฅ โ (โฅโ๐ป) โ ๐ฅ โ (โฅโ๐บ)))) |
44 | 43 | pm2.43d 53 |
. . . . 5
โข ((๐ฅ โ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) โ (๐ฅ โ (โฅโ๐ป) โ ๐ฅ โ (โฅโ๐บ))) |
45 | 44 | alimi 1814 |
. . . 4
โข
(โ๐ฅ(๐ฅ โ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) โ โ๐ฅ(๐ฅ โ (โฅโ๐ป) โ ๐ฅ โ (โฅโ๐บ))) |
46 | | df-ral 3062 |
. . . 4
โข
(โ๐ฅ โ
โ (normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)) โ โ๐ฅ(๐ฅ โ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)))) |
47 | | dfss2 3931 |
. . . 4
โข
((โฅโ๐ป)
โ (โฅโ๐บ)
โ โ๐ฅ(๐ฅ โ (โฅโ๐ป) โ ๐ฅ โ (โฅโ๐บ))) |
48 | 45, 46, 47 | 3imtr4i 292 |
. . 3
โข
(โ๐ฅ โ
โ (normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)) โ (โฅโ๐ป) โ (โฅโ๐บ)) |
49 | 2, 1 | chsscon3i 30445 |
. . 3
โข (๐บ โ ๐ป โ (โฅโ๐ป) โ (โฅโ๐บ)) |
50 | 48, 49 | sylibr 233 |
. 2
โข
(โ๐ฅ โ
โ (normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ)) โ ๐บ โ ๐ป) |
51 | 9, 50 | impbii 208 |
1
โข (๐บ โ ๐ป โ โ๐ฅ โ โ
(normโโ((projโโ๐บ)โ๐ฅ)) โค
(normโโ((projโโ๐ป)โ๐ฅ))) |