Step | Hyp | Ref
| Expression |
1 | | pjco.1 |
. . . . . . 7
โข ๐บ โ
Cโ |
2 | | pjco.2 |
. . . . . . 7
โข ๐ป โ
Cโ |
3 | 1, 2 | pjcoi 31142 |
. . . . . 6
โข (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ๐บ)โ((projโโ๐ป)โ๐ฅ))) |
4 | 3 | adantl 483 |
. . . . 5
โข ((๐บ โ ๐ป โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ๐บ)โ((projโโ๐ป)โ๐ฅ))) |
5 | | 2fveq3 6848 |
. . . . . . . . 9
โข (๐ฅ = if(๐ฅ โ โ, ๐ฅ, 0โ) โ
((projโโ๐บ)โ((projโโ๐ป)โ๐ฅ)) = ((projโโ๐บ)โ((projโโ๐ป)โif(๐ฅ โ โ, ๐ฅ, 0โ)))) |
6 | | fveq2 6843 |
. . . . . . . . 9
โข (๐ฅ = if(๐ฅ โ โ, ๐ฅ, 0โ) โ
((projโโ๐บ)โ๐ฅ) = ((projโโ๐บ)โif(๐ฅ โ โ, ๐ฅ, 0โ))) |
7 | 5, 6 | eqeq12d 2749 |
. . . . . . . 8
โข (๐ฅ = if(๐ฅ โ โ, ๐ฅ, 0โ) โ
(((projโโ๐บ)โ((projโโ๐ป)โ๐ฅ)) = ((projโโ๐บ)โ๐ฅ) โ ((projโโ๐บ)โ((projโโ๐ป)โif(๐ฅ โ โ, ๐ฅ, 0โ))) =
((projโโ๐บ)โif(๐ฅ โ โ, ๐ฅ, 0โ)))) |
8 | 7 | imbi2d 341 |
. . . . . . 7
โข (๐ฅ = if(๐ฅ โ โ, ๐ฅ, 0โ) โ ((๐บ โ ๐ป โ
((projโโ๐บ)โ((projโโ๐ป)โ๐ฅ)) = ((projโโ๐บ)โ๐ฅ)) โ (๐บ โ ๐ป โ ((projโโ๐บ)โ((projโโ๐ป)โif(๐ฅ โ โ, ๐ฅ, 0โ))) =
((projโโ๐บ)โif(๐ฅ โ โ, ๐ฅ, 0โ))))) |
9 | | ifhvhv0 30006 |
. . . . . . . 8
โข if(๐ฅ โ โ, ๐ฅ, 0โ) โ
โ |
10 | 1, 9, 2 | pjss2i 30664 |
. . . . . . 7
โข (๐บ โ ๐ป โ
((projโโ๐บ)โ((projโโ๐ป)โif(๐ฅ โ โ, ๐ฅ, 0โ))) =
((projโโ๐บ)โif(๐ฅ โ โ, ๐ฅ, 0โ))) |
11 | 8, 10 | dedth 4545 |
. . . . . 6
โข (๐ฅ โ โ โ (๐บ โ ๐ป โ
((projโโ๐บ)โ((projโโ๐ป)โ๐ฅ)) = ((projโโ๐บ)โ๐ฅ))) |
12 | 11 | impcom 409 |
. . . . 5
โข ((๐บ โ ๐ป โง ๐ฅ โ โ) โ
((projโโ๐บ)โ((projโโ๐ป)โ๐ฅ)) = ((projโโ๐บ)โ๐ฅ)) |
13 | 4, 12 | eqtrd 2773 |
. . . 4
โข ((๐บ โ ๐ป โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ๐บ)โ๐ฅ)) |
14 | 13 | ralrimiva 3140 |
. . 3
โข (๐บ โ ๐ป โ โ๐ฅ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ๐บ)โ๐ฅ)) |
15 | 1 | pjfi 30688 |
. . . . 5
โข
(projโโ๐บ): โโถ โ |
16 | 2 | pjfi 30688 |
. . . . 5
โข
(projโโ๐ป): โโถ โ |
17 | 15, 16 | hocofi 30750 |
. . . 4
โข
((projโโ๐บ) โ
(projโโ๐ป)): โโถ โ |
18 | 17, 15 | hoeqi 30745 |
. . 3
โข
(โ๐ฅ โ
โ (((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ๐บ)โ๐ฅ) โ
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ)) |
19 | 14, 18 | sylib 217 |
. 2
โข (๐บ โ ๐ป โ
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ)) |
20 | | fveq1 6842 |
. . . . . . . . . . . 12
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ) = ((projโโ๐บ)โ๐ฆ)) |
21 | 20 | oveq2d 7374 |
. . . . . . . . . . 11
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ) โ (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih
((projโโ๐บ)โ๐ฆ))) |
22 | 21 | ad2antlr 726 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ)) โง ๐ฆ โ โ) โ (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih
((projโโ๐บ)โ๐ฆ))) |
23 | 2, 1 | pjadjcoi 31145 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ))) |
24 | 23 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ)) โง ๐ฆ โ โ) โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ))) |
25 | 1 | pjadji 30669 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(((projโโ๐บ)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((projโโ๐บ)โ๐ฆ))) |
26 | 25 | adantlr 714 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ)) โง ๐ฆ โ โ) โ
(((projโโ๐บ)โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((projโโ๐บ)โ๐ฆ))) |
27 | 22, 24, 26 | 3eqtr4d 2783 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ)) โง ๐ฆ โ โ) โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) =
(((projโโ๐บ)โ๐ฅ) ยทih ๐ฆ)) |
28 | 27 | exp31 421 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ) โ (๐ฆ โ โ โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) =
(((projโโ๐บ)โ๐ฅ) ยทih ๐ฆ)))) |
29 | 28 | ralrimdv 3146 |
. . . . . . 7
โข (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ) โ โ๐ฆ โ โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) =
(((projโโ๐บ)โ๐ฅ) ยทih ๐ฆ))) |
30 | 2, 1 | pjcohcli 31144 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) โ โ) |
31 | 1 | pjhcli 30402 |
. . . . . . . 8
โข (๐ฅ โ โ โ
((projโโ๐บ)โ๐ฅ) โ โ) |
32 | | hial2eq 30090 |
. . . . . . . 8
โข
(((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) โ โ โง
((projโโ๐บ)โ๐ฅ) โ โ) โ (โ๐ฆ โ โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) =
(((projโโ๐บ)โ๐ฅ) ยทih ๐ฆ) โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) = ((projโโ๐บ)โ๐ฅ))) |
33 | 30, 31, 32 | syl2anc 585 |
. . . . . . 7
โข (๐ฅ โ โ โ
(โ๐ฆ โ โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) =
(((projโโ๐บ)โ๐ฅ) ยทih ๐ฆ) โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) = ((projโโ๐บ)โ๐ฅ))) |
34 | 29, 33 | sylibd 238 |
. . . . . 6
โข (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ) โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) = ((projโโ๐บ)โ๐ฅ))) |
35 | 34 | com12 32 |
. . . . 5
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ) โ (๐ฅ โ โ โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) = ((projโโ๐บ)โ๐ฅ))) |
36 | 35 | ralrimiv 3139 |
. . . 4
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ) โ โ๐ฅ โ โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) = ((projโโ๐บ)โ๐ฅ)) |
37 | 16, 15 | hocofi 30750 |
. . . . 5
โข
((projโโ๐ป) โ
(projโโ๐บ)): โโถ โ |
38 | 37, 15 | hoeqi 30745 |
. . . 4
โข
(โ๐ฅ โ
โ (((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) = ((projโโ๐บ)โ๐ฅ) โ
((projโโ๐ป) โ
(projโโ๐บ)) = (projโโ๐บ)) |
39 | 36, 38 | sylib 217 |
. . 3
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ) โ
((projโโ๐ป) โ
(projโโ๐บ)) = (projโโ๐บ)) |
40 | 1, 2 | pjss1coi 31147 |
. . 3
โข (๐บ โ ๐ป โ
((projโโ๐ป) โ
(projโโ๐บ)) = (projโโ๐บ)) |
41 | 39, 40 | sylibr 233 |
. 2
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ) โ ๐บ โ ๐ป) |
42 | 19, 41 | impbii 208 |
1
โข (๐บ โ ๐ป โ
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ๐บ)) |