Step | Hyp | Ref
| Expression |
1 | | pjsslem.1 |
. . . . . 6
โข ๐บ โ
Cโ |
2 | | pjidm.2 |
. . . . . 6
โข ๐ด โ โ |
3 | 1, 2 | pjclii 30705 |
. . . . 5
โข
((projโโ๐บ)โ๐ด) โ ๐บ |
4 | | pjidm.1 |
. . . . . . 7
โข ๐ป โ
Cโ |
5 | 4, 2 | pjclii 30705 |
. . . . . 6
โข
((projโโ๐ป)โ๐ด) โ ๐ป |
6 | | ssel 3976 |
. . . . . 6
โข (๐ป โ ๐บ โ
(((projโโ๐ป)โ๐ด) โ ๐ป โ
((projโโ๐ป)โ๐ด) โ ๐บ)) |
7 | 5, 6 | mpi 20 |
. . . . 5
โข (๐ป โ ๐บ โ
((projโโ๐ป)โ๐ด) โ ๐บ) |
8 | 1 | chshii 30511 |
. . . . . 6
โข ๐บ โ
Sโ |
9 | | shsubcl 30504 |
. . . . . 6
โข ((๐บ โ
Sโ โง ((projโโ๐บ)โ๐ด) โ ๐บ โง ((projโโ๐ป)โ๐ด) โ ๐บ) โ
(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ ๐บ) |
10 | 8, 9 | mp3an1 1449 |
. . . . 5
โข
((((projโโ๐บ)โ๐ด) โ ๐บ โง ((projโโ๐ป)โ๐ด) โ ๐บ) โ
(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ ๐บ) |
11 | 3, 7, 10 | sylancr 588 |
. . . 4
โข (๐ป โ ๐บ โ
(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ ๐บ) |
12 | 4, 2, 1 | pjsslem 30963 |
. . . . 5
โข
(((projโโ(โฅโ๐ป))โ๐ด) โโ
((projโโ(โฅโ๐บ))โ๐ด)) = (((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) |
13 | 4, 1 | chsscon3i 30745 |
. . . . . 6
โข (๐ป โ ๐บ โ (โฅโ๐บ) โ (โฅโ๐ป)) |
14 | 4 | choccli 30591 |
. . . . . . . 8
โข
(โฅโ๐ป)
โ Cโ |
15 | 14, 2 | pjclii 30705 |
. . . . . . 7
โข
((projโโ(โฅโ๐ป))โ๐ด) โ (โฅโ๐ป) |
16 | 1 | choccli 30591 |
. . . . . . . . 9
โข
(โฅโ๐บ)
โ Cโ |
17 | 16, 2 | pjclii 30705 |
. . . . . . . 8
โข
((projโโ(โฅโ๐บ))โ๐ด) โ (โฅโ๐บ) |
18 | | ssel 3976 |
. . . . . . . 8
โข
((โฅโ๐บ)
โ (โฅโ๐ป)
โ (((projโโ(โฅโ๐บ))โ๐ด) โ (โฅโ๐บ) โ
((projโโ(โฅโ๐บ))โ๐ด) โ (โฅโ๐ป))) |
19 | 17, 18 | mpi 20 |
. . . . . . 7
โข
((โฅโ๐บ)
โ (โฅโ๐ป)
โ ((projโโ(โฅโ๐บ))โ๐ด) โ (โฅโ๐ป)) |
20 | 14 | chshii 30511 |
. . . . . . . 8
โข
(โฅโ๐ป)
โ Sโ |
21 | | shsubcl 30504 |
. . . . . . . 8
โข
(((โฅโ๐ป)
โ Sโ โง
((projโโ(โฅโ๐ป))โ๐ด) โ (โฅโ๐ป) โง
((projโโ(โฅโ๐บ))โ๐ด) โ (โฅโ๐ป)) โ
(((projโโ(โฅโ๐ป))โ๐ด) โโ
((projโโ(โฅโ๐บ))โ๐ด)) โ (โฅโ๐ป)) |
22 | 20, 21 | mp3an1 1449 |
. . . . . . 7
โข
((((projโโ(โฅโ๐ป))โ๐ด) โ (โฅโ๐ป) โง
((projโโ(โฅโ๐บ))โ๐ด) โ (โฅโ๐ป)) โ
(((projโโ(โฅโ๐ป))โ๐ด) โโ
((projโโ(โฅโ๐บ))โ๐ด)) โ (โฅโ๐ป)) |
23 | 15, 19, 22 | sylancr 588 |
. . . . . 6
โข
((โฅโ๐บ)
โ (โฅโ๐ป)
โ (((projโโ(โฅโ๐ป))โ๐ด) โโ
((projโโ(โฅโ๐บ))โ๐ด)) โ (โฅโ๐ป)) |
24 | 13, 23 | sylbi 216 |
. . . . 5
โข (๐ป โ ๐บ โ
(((projโโ(โฅโ๐ป))โ๐ด) โโ
((projโโ(โฅโ๐บ))โ๐ด)) โ (โฅโ๐ป)) |
25 | 12, 24 | eqeltrrid 2839 |
. . . 4
โข (๐ป โ ๐บ โ
(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ (โฅโ๐ป)) |
26 | 11, 25 | jca 513 |
. . 3
โข (๐ป โ ๐บ โ
((((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ ๐บ โง
(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ (โฅโ๐ป))) |
27 | | elin 3965 |
. . . 4
โข
((((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ (๐บ โฉ (โฅโ๐ป)) โ
((((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ ๐บ โง
(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ (โฅโ๐ป))) |
28 | 1, 14 | chincli 30744 |
. . . . 5
โข (๐บ โฉ (โฅโ๐ป)) โ
Cโ |
29 | 1, 2 | pjhclii 30706 |
. . . . . 6
โข
((projโโ๐บ)โ๐ด) โ โ |
30 | 4, 2 | pjhclii 30706 |
. . . . . 6
โข
((projโโ๐ป)โ๐ด) โ โ |
31 | 29, 30 | hvsubcli 30305 |
. . . . 5
โข
(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ โ |
32 | 28, 31 | pjchi 30716 |
. . . 4
โข
((((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ (๐บ โฉ (โฅโ๐ป)) โ
((projโโ(๐บ โฉ (โฅโ๐ป)))โ(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด))) = (((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด))) |
33 | 27, 32 | bitr3i 277 |
. . 3
โข
(((((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ ๐บ โง
(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) โ (โฅโ๐ป)) โ
((projโโ(๐บ โฉ (โฅโ๐ป)))โ(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด))) = (((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด))) |
34 | 26, 33 | sylib 217 |
. 2
โข (๐ป โ ๐บ โ
((projโโ(๐บ โฉ (โฅโ๐ป)))โ(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด))) = (((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด))) |
35 | 28, 29, 30 | pjsubii 30962 |
. . 3
โข
((projโโ(๐บ โฉ (โฅโ๐ป)))โ(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด))) = (((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐บ)โ๐ด)) โโ
((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด))) |
36 | 28, 29 | pjhclii 30706 |
. . . . 5
โข
((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐บ)โ๐ด)) โ โ |
37 | 28, 30 | pjhclii 30706 |
. . . . 5
โข
((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด)) โ โ |
38 | 36, 37 | hvsubvali 30304 |
. . . 4
โข
(((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐บ)โ๐ด)) โโ
((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด))) = (((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐บ)โ๐ด)) +โ (-1
ยทโ ((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด)))) |
39 | | inss1 4229 |
. . . . . . 7
โข (๐บ โฉ (โฅโ๐ป)) โ ๐บ |
40 | 28, 2, 1 | pjss2i 30964 |
. . . . . . 7
โข ((๐บ โฉ (โฅโ๐ป)) โ ๐บ โ
((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐บ)โ๐ด)) = ((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด)) |
41 | 39, 40 | ax-mp 5 |
. . . . . 6
โข
((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐บ)โ๐ด)) = ((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) |
42 | 4 | chshii 30511 |
. . . . . . . . . . . 12
โข ๐ป โ
Sโ |
43 | | shococss 30578 |
. . . . . . . . . . . 12
โข (๐ป โ
Sโ โ ๐ป โ (โฅโ(โฅโ๐ป))) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . 11
โข ๐ป โ
(โฅโ(โฅโ๐ป)) |
45 | | inss2 4230 |
. . . . . . . . . . . 12
โข (๐บ โฉ (โฅโ๐ป)) โ (โฅโ๐ป) |
46 | 28, 14 | chsscon3i 30745 |
. . . . . . . . . . . 12
โข ((๐บ โฉ (โฅโ๐ป)) โ (โฅโ๐ป) โ
(โฅโ(โฅโ๐ป)) โ (โฅโ(๐บ โฉ (โฅโ๐ป)))) |
47 | 45, 46 | mpbi 229 |
. . . . . . . . . . 11
โข
(โฅโ(โฅโ๐ป)) โ (โฅโ(๐บ โฉ (โฅโ๐ป))) |
48 | 44, 47 | sstri 3992 |
. . . . . . . . . 10
โข ๐ป โ (โฅโ(๐บ โฉ (โฅโ๐ป))) |
49 | 48, 5 | sselii 3980 |
. . . . . . . . 9
โข
((projโโ๐ป)โ๐ด) โ (โฅโ(๐บ โฉ (โฅโ๐ป))) |
50 | 28, 30 | pjoc2i 30722 |
. . . . . . . . 9
โข
(((projโโ๐ป)โ๐ด) โ (โฅโ(๐บ โฉ (โฅโ๐ป))) โ
((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด)) = 0โ) |
51 | 49, 50 | mpbi 229 |
. . . . . . . 8
โข
((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด)) = 0โ |
52 | 51 | oveq2i 7420 |
. . . . . . 7
โข (-1
ยทโ ((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด))) = (-1 ยทโ
0โ) |
53 | | neg1cn 12326 |
. . . . . . . 8
โข -1 โ
โ |
54 | | hvmul0 30308 |
. . . . . . . 8
โข (-1
โ โ โ (-1 ยทโ
0โ) = 0โ) |
55 | 53, 54 | ax-mp 5 |
. . . . . . 7
โข (-1
ยทโ 0โ) =
0โ |
56 | 52, 55 | eqtri 2761 |
. . . . . 6
โข (-1
ยทโ ((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด))) = 0โ |
57 | 41, 56 | oveq12i 7421 |
. . . . 5
โข
(((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐บ)โ๐ด)) +โ (-1
ยทโ ((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด)))) = (((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) +โ
0โ) |
58 | 28, 2 | pjhclii 30706 |
. . . . . 6
โข
((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) โ โ |
59 | | ax-hvaddid 30288 |
. . . . . 6
โข
(((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) โ โ โ
(((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) +โ 0โ)
= ((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด)) |
60 | 58, 59 | ax-mp 5 |
. . . . 5
โข
(((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) +โ 0โ)
= ((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) |
61 | 57, 60 | eqtri 2761 |
. . . 4
โข
(((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐บ)โ๐ด)) +โ (-1
ยทโ ((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด)))) = ((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) |
62 | 38, 61 | eqtri 2761 |
. . 3
โข
(((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐บ)โ๐ด)) โโ
((projโโ(๐บ โฉ (โฅโ๐ป)))โ((projโโ๐ป)โ๐ด))) = ((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) |
63 | 35, 62 | eqtri 2761 |
. 2
โข
((projโโ(๐บ โฉ (โฅโ๐ป)))โ(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด))) = ((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด) |
64 | 34, 63 | eqtr3di 2788 |
1
โข (๐ป โ ๐บ โ
(((projโโ๐บ)โ๐ด) โโ
((projโโ๐ป)โ๐ด)) = ((projโโ(๐บ โฉ (โฅโ๐ป)))โ๐ด)) |