Step | Hyp | Ref
| Expression |
1 | | pjclem1.1 |
. . . . . . . 8
โข ๐บ โ
Cโ |
2 | | pjclem1.2 |
. . . . . . . 8
โข ๐ป โ
Cโ |
3 | 1, 2 | pjcocli 31412 |
. . . . . . 7
โข (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐บ) |
4 | 3 | adantl 483 |
. . . . . 6
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐บ) |
5 | 2, 1 | pjcocli 31412 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) โ ๐ป) |
6 | | fveq1 6891 |
. . . . . . . . 9
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = (((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ)) |
7 | 6 | eleq1d 2819 |
. . . . . . . 8
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) โ ๐ป)) |
8 | 5, 7 | imbitrrid 245 |
. . . . . . 7
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป)) |
9 | 8 | imp 408 |
. . . . . 6
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป) |
10 | 4, 9 | elind 4195 |
. . . . 5
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ (๐บ โฉ ๐ป)) |
11 | 1, 2 | pjcohcli 31413 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ) |
12 | | hvsubcl 30270 |
. . . . . . . 8
โข ((๐ฅ โ โ โง
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ) โ (๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) โ โ) |
13 | 11, 12 | mpdan 686 |
. . . . . . 7
โข (๐ฅ โ โ โ (๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) โ โ) |
14 | 13 | adantl 483 |
. . . . . 6
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ (๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) โ โ) |
15 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ ๐ฅ โ โ) |
16 | 11 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ) |
17 | 1, 2 | chincli 30713 |
. . . . . . . . . . . . . 14
โข (๐บ โฉ ๐ป) โ
Cโ |
18 | 17 | cheli 30485 |
. . . . . . . . . . . . 13
โข (๐ฆ โ (๐บ โฉ ๐ป) โ ๐ฆ โ โ) |
19 | 18 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ ๐ฆ โ โ) |
20 | 15, 16, 19 | 3jca 1129 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ (๐ฅ โ โ โง
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ)) |
21 | 20 | adantl 483 |
. . . . . . . . . 10
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ (๐ฅ โ โ โง
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ)) |
22 | | his2sub 30345 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ) โ ((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = ((๐ฅ ยทih ๐ฆ) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ))) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ ((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = ((๐ฅ ยทih ๐ฆ) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ))) |
24 | 6 | oveq1d 7424 |
. . . . . . . . . . 11
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ)) |
25 | 2, 1 | pjadjcoi 31414 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ))) |
26 | 18, 25 | sylan2 594 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ))) |
27 | 1, 2 | pjclem4a 31451 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ (๐บ โฉ ๐ป) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ) = ๐ฆ) |
28 | 27 | oveq2d 7425 |
. . . . . . . . . . . . 13
โข (๐ฆ โ (๐บ โฉ ๐ป) โ (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) |
29 | 28 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) |
30 | 26, 29 | eqtrd 2773 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih ๐ฆ)) |
31 | 24, 30 | sylan9eq 2793 |
. . . . . . . . . 10
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih ๐ฆ)) |
32 | 31 | oveq1d 7424 |
. . . . . . . . 9
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ
(((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ)) = ((๐ฅ ยทih ๐ฆ) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ))) |
33 | 11, 18 | anim12i 614 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ)) |
34 | 33 | adantl 483 |
. . . . . . . . . . 11
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ)) |
35 | | hicl 30333 |
. . . . . . . . . . 11
โข
(((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
โ) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
โ) |
37 | 36 | subidd 11559 |
. . . . . . . . 9
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ
(((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ)) = 0) |
38 | 23, 32, 37 | 3eqtr2d 2779 |
. . . . . . . 8
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ ((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0) |
39 | 38 | expr 458 |
. . . . . . 7
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ (๐ฆ โ (๐บ โฉ ๐ป) โ ((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0)) |
40 | 39 | ralrimiv 3146 |
. . . . . 6
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ โ๐ฆ โ (๐บ โฉ ๐ป)((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0) |
41 | 17 | chshii 30480 |
. . . . . . 7
โข (๐บ โฉ ๐ป) โ
Sโ |
42 | | shocel 30535 |
. . . . . . 7
โข ((๐บ โฉ ๐ป) โ Sโ
โ ((๐ฅ
โโ (((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) โ (โฅโ(๐บ โฉ ๐ป)) โ ((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) โ โ โง โ๐ฆ โ (๐บ โฉ ๐ป)((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0))) |
43 | 41, 42 | ax-mp 5 |
. . . . . 6
โข ((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) โ (โฅโ(๐บ โฉ ๐ป)) โ ((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) โ โ โง โ๐ฆ โ (๐บ โฉ ๐ป)((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0)) |
44 | 14, 40, 43 | sylanbrc 584 |
. . . . 5
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ (๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) โ (โฅโ(๐บ โฉ ๐ป))) |
45 | 17 | pjvi 30958 |
. . . . 5
โข
(((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ (๐บ โฉ ๐ป) โง (๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) โ (โฅโ(๐บ โฉ ๐ป))) โ
((projโโ(๐บ โฉ ๐ป))โ((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
(((projโโ๐บ) โ (projโโ๐ป))โ๐ฅ)))) = (((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) |
46 | 10, 44, 45 | syl2anc 585 |
. . . 4
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
((projโโ(๐บ โฉ ๐ป))โ((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
(((projโโ๐บ) โ (projโโ๐ป))โ๐ฅ)))) = (((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) |
47 | | id 22 |
. . . . . . . 8
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
48 | | hvaddsub12 30291 |
. . . . . . . 8
โข
(((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฅ โ โ โง
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ))) = (๐ฅ +โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)))) |
49 | 11, 47, 11, 48 | syl3anc 1372 |
. . . . . . 7
โข (๐ฅ โ โ โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ))) = (๐ฅ +โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)))) |
50 | | hvsubid 30279 |
. . . . . . . . 9
โข
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) = 0โ) |
51 | 11, 50 | syl 17 |
. . . . . . . 8
โข (๐ฅ โ โ โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) = 0โ) |
52 | 51 | oveq2d 7425 |
. . . . . . 7
โข (๐ฅ โ โ โ (๐ฅ +โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ))) = (๐ฅ +โ
0โ)) |
53 | | ax-hvaddid 30257 |
. . . . . . 7
โข (๐ฅ โ โ โ (๐ฅ +โ
0โ) = ๐ฅ) |
54 | 49, 52, 53 | 3eqtrd 2777 |
. . . . . 6
โข (๐ฅ โ โ โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ))) = ๐ฅ) |
55 | 54 | fveq2d 6896 |
. . . . 5
โข (๐ฅ โ โ โ
((projโโ(๐บ โฉ ๐ป))โ((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
(((projโโ๐บ) โ (projโโ๐ป))โ๐ฅ)))) = ((projโโ(๐บ โฉ ๐ป))โ๐ฅ)) |
56 | 55 | adantl 483 |
. . . 4
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
((projโโ(๐บ โฉ ๐ป))โ((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
(((projโโ๐บ) โ (projโโ๐ป))โ๐ฅ)))) = ((projโโ(๐บ โฉ ๐ป))โ๐ฅ)) |
57 | 46, 56 | eqtr3d 2775 |
. . 3
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ(๐บ โฉ ๐ป))โ๐ฅ)) |
58 | 57 | ralrimiva 3147 |
. 2
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ โ๐ฅ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ(๐บ โฉ ๐ป))โ๐ฅ)) |
59 | 1 | pjfi 30957 |
. . . 4
โข
(projโโ๐บ): โโถ โ |
60 | 2 | pjfi 30957 |
. . . 4
โข
(projโโ๐ป): โโถ โ |
61 | 59, 60 | hocofi 31019 |
. . 3
โข
((projโโ๐บ) โ
(projโโ๐ป)): โโถ โ |
62 | 17 | pjfi 30957 |
. . 3
โข
(projโโ(๐บ โฉ ๐ป)): โโถ โ |
63 | 61, 62 | hoeqi 31014 |
. 2
โข
(โ๐ฅ โ
โ (((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ(๐บ โฉ ๐ป))โ๐ฅ) โ
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ(๐บ โฉ ๐ป))) |
64 | 58, 63 | sylib 217 |
1
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ(๐บ โฉ ๐ป))) |