Step | Hyp | Ref
| Expression |
1 | | fveq1 6846 |
. . . . . . . . . . 11
โข
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป)) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ) = ((((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))โ๐ฆ)) |
2 | 1 | oveq2d 7378 |
. . . . . . . . . 10
โข
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป)) โ (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih
((((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))โ๐ฆ))) |
3 | 2 | adantl 483 |
. . . . . . . . 9
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih
((((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))โ๐ฆ))) |
4 | 3 | ad2antlr 726 |
. . . . . . . 8
โข (((๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป)))) โง ๐ฆ โ โ) โ (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih
((((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))โ๐ฆ))) |
5 | | pjadj2co.1 |
. . . . . . . . . . . . 13
โข ๐น โ
Cโ |
6 | | pjadj2co.2 |
. . . . . . . . . . . . 13
โข ๐บ โ
Cโ |
7 | 5, 6 | chincli 30444 |
. . . . . . . . . . . 12
โข (๐น โฉ ๐บ) โ
Cโ |
8 | | pjadj2co.3 |
. . . . . . . . . . . 12
โข ๐ป โ
Cโ |
9 | 7, 8 | chincli 30444 |
. . . . . . . . . . 11
โข ((๐น โฉ ๐บ) โฉ ๐ป) โ
Cโ |
10 | 9 | pjadji 30669 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฆ))) |
11 | 10 | adantlr 714 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป)))) โง ๐ฆ โ โ) โ
(((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฆ))) |
12 | 5, 6, 8 | pj3i 31192 |
. . . . . . . . . . . 12
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (projโโ((๐น โฉ ๐บ) โฉ ๐ป))) |
13 | 12 | fveq1d 6849 |
. . . . . . . . . . 11
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ)) |
14 | 13 | oveq1d 7377 |
. . . . . . . . . 10
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
(((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ) ยทih ๐ฆ)) |
15 | 14 | ad2antlr 726 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป)))) โง ๐ฆ โ โ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
(((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ) ยทih ๐ฆ)) |
16 | 12 | fveq1d 6849 |
. . . . . . . . . . 11
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ) = ((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฆ)) |
17 | 16 | oveq2d 7378 |
. . . . . . . . . 10
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih
((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฆ))) |
18 | 17 | ad2antlr 726 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป)))) โง ๐ฆ โ โ) โ (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih
((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฆ))) |
19 | 11, 15, 18 | 3eqtr4d 2787 |
. . . . . . . 8
โข (((๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป)))) โง ๐ฆ โ โ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ))) |
20 | 8, 5, 6 | pjadj2coi 31188 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))โ๐ฆ))) |
21 | 20 | adantlr 714 |
. . . . . . . 8
โข (((๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป)))) โง ๐ฆ โ โ) โ
(((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))โ๐ฆ))) |
22 | 4, 19, 21 | 3eqtr4d 2787 |
. . . . . . 7
โข (((๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป)))) โง ๐ฆ โ โ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
(((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ)) |
23 | 22 | exp31 421 |
. . . . . 6
โข (๐ฅ โ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ (๐ฆ โ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
(((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ)))) |
24 | 23 | ralrimdv 3150 |
. . . . 5
โข (๐ฅ โ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ โ๐ฆ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
(((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ))) |
25 | 5 | pjfi 30688 |
. . . . . . . 8
โข
(projโโ๐น): โโถ โ |
26 | 6 | pjfi 30688 |
. . . . . . . 8
โข
(projโโ๐บ): โโถ โ |
27 | 25, 26 | hocofi 30750 |
. . . . . . 7
โข
((projโโ๐น) โ
(projโโ๐บ)): โโถ โ |
28 | 8 | pjfi 30688 |
. . . . . . 7
โข
(projโโ๐ป): โโถ โ |
29 | 27, 28 | hococli 30749 |
. . . . . 6
โข (๐ฅ โ โ โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ) |
30 | 28, 25 | hocofi 30750 |
. . . . . . 7
โข
((projโโ๐ป) โ
(projโโ๐น)): โโถ โ |
31 | 30, 26 | hococli 30749 |
. . . . . 6
โข (๐ฅ โ โ โ
((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) โ โ) |
32 | | hial2eq 30090 |
. . . . . 6
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ โง
((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) โ โ) โ (โ๐ฆ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
(((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ))) |
33 | 29, 31, 32 | syl2anc 585 |
. . . . 5
โข (๐ฅ โ โ โ
(โ๐ฆ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
(((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ))) |
34 | 24, 33 | sylibd 238 |
. . . 4
โข (๐ฅ โ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ))) |
35 | 34 | com12 32 |
. . 3
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ (๐ฅ โ โ โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ))) |
36 | 35 | ralrimiv 3143 |
. 2
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ โ๐ฅ โ โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ)) |
37 | 27, 28 | hocofi 30750 |
. . 3
โข
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)): โโถ โ |
38 | 30, 26 | hocofi 30750 |
. . 3
โข
(((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ)): โโถ โ |
39 | 37, 38 | hoeqi 30745 |
. 2
โข
(โ๐ฅ โ
โ ((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))โ๐ฅ) โ
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))) |
40 | 36, 39 | sylib 217 |
1
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐บ) โ
(projโโ๐น)) โ
(projโโ๐ป))) โ
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐น)) โ
(projโโ๐บ))) |