Step | Hyp | Ref
| Expression |
1 | | pjclem1.1 |
. . . . . . . 8
โข ๐บ โ
Cโ |
2 | | pjclem1.2 |
. . . . . . . 8
โข ๐ป โ
Cโ |
3 | 1, 2 | pjcocli 31143 |
. . . . . . 7
โข (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐บ) |
4 | 3 | adantl 483 |
. . . . . 6
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐บ) |
5 | 2, 1 | pjcocli 31143 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) โ ๐ป) |
6 | | fveq1 6846 |
. . . . . . . . 9
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = (((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ)) |
7 | 6 | eleq1d 2823 |
. . . . . . . 8
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป โ
(((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) โ ๐ป)) |
8 | 5, 7 | syl5ibr 246 |
. . . . . . 7
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป)) |
9 | 8 | imp 408 |
. . . . . 6
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป) |
10 | 4, 9 | elind 4159 |
. . . . 5
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ (๐บ โฉ ๐ป)) |
11 | 1, 2 | pjcohcli 31144 |
. . . . . . . 8
โข (๐ฅ โ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ) |
12 | | hvsubcl 30001 |
. . . . . . . 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 30444 |
. . . . . . . . . . . . . 14
โข (๐บ โฉ ๐ป) โ
Cโ |
18 | 17 | cheli 30216 |
. . . . . . . . . . . . 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 30076 |
. . . . . . . . . 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 7377 |
. . . . . . . . . . 11
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ)) |
25 | 2, 1 | pjadjcoi 31145 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ))) |
26 | 18, 25 | sylan2 594 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ))) |
27 | 1, 2 | pjclem4a 31182 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ (๐บ โฉ ๐ป) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ) = ๐ฆ) |
28 | 27 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ฆ โ (๐บ โฉ ๐ป) โ (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) |
29 | 28 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ (๐ฅ ยทih
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) |
30 | 26, 29 | eqtrd 2777 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป)) โ
((((projโโ๐ป) โ
(projโโ๐บ))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih ๐ฆ)) |
31 | 24, 30 | sylan9eq 2797 |
. . . . . . . . . 10
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih ๐ฆ)) |
32 | 31 | oveq1d 7377 |
. . . . . . . . 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 30064 |
. . . . . . . . . . 11
โข
(((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
โ) |
36 | 34, 35 | syl 17 |
. . . . . . . . . 10
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
โ) |
37 | 36 | subidd 11507 |
. . . . . . . . 9
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง (๐ฅ โ โ โง ๐ฆ โ (๐บ โฉ ๐ป))) โ
(((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ)) = 0) |
38 | 23, 32, 37 | 3eqtr2d 2783 |
. . . . . . . 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 3143 |
. . . . . 6
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ โ๐ฆ โ (๐บ โฉ ๐ป)((๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0) |
41 | 17 | chshii 30211 |
. . . . . . 7
โข (๐บ โฉ ๐ป) โ
Sโ |
42 | | shocel 30266 |
. . . . . . 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 30689 |
. . . . 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 30022 |
. . . . . . . 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 30010 |
. . . . . . . . 9
โข
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โ โ โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) = 0โ) |
51 | 11, 50 | syl 17 |
. . . . . . . 8
โข (๐ฅ โ โ โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ)) = 0โ) |
52 | 51 | oveq2d 7378 |
. . . . . . 7
โข (๐ฅ โ โ โ (๐ฅ +โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ))) = (๐ฅ +โ
0โ)) |
53 | | ax-hvaddid 29988 |
. . . . . . 7
โข (๐ฅ โ โ โ (๐ฅ +โ
0โ) = ๐ฅ) |
54 | 49, 52, 53 | 3eqtrd 2781 |
. . . . . 6
โข (๐ฅ โ โ โ
((((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ))) = ๐ฅ) |
55 | 54 | fveq2d 6851 |
. . . . 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 2779 |
. . 3
โข
((((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โง ๐ฅ โ โ) โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ(๐บ โฉ ๐ป))โ๐ฅ)) |
58 | 57 | ralrimiva 3144 |
. 2
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ โ๐ฅ โ โ
(((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ(๐บ โฉ ๐ป))โ๐ฅ)) |
59 | 1 | pjfi 30688 |
. . . 4
โข
(projโโ๐บ): โโถ โ |
60 | 2 | pjfi 30688 |
. . . 4
โข
(projโโ๐ป): โโถ โ |
61 | 59, 60 | hocofi 30750 |
. . 3
โข
((projโโ๐บ) โ
(projโโ๐ป)): โโถ โ |
62 | 17 | pjfi 30688 |
. . 3
โข
(projโโ(๐บ โฉ ๐ป)): โโถ โ |
63 | 61, 62 | hoeqi 30745 |
. 2
โข
(โ๐ฅ โ
โ (((projโโ๐บ) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ(๐บ โฉ ๐ป))โ๐ฅ) โ
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ(๐บ โฉ ๐ป))) |
64 | 58, 63 | sylib 217 |
1
โข
(((projโโ๐บ) โ
(projโโ๐ป)) = ((projโโ๐ป) โ
(projโโ๐บ)) โ
((projโโ๐บ) โ
(projโโ๐ป)) = (projโโ(๐บ โฉ ๐ป))) |