Step | Hyp | Ref
| Expression |
1 | | pjadj2co.1 |
. . . . . . . . . 10
โข ๐น โ
Cโ |
2 | | pjadj2co.2 |
. . . . . . . . . 10
โข ๐บ โ
Cโ |
3 | | pjadj2co.3 |
. . . . . . . . . 10
โข ๐ป โ
Cโ |
4 | 1, 2, 3 | pj2cocli 31189 |
. . . . . . . . 9
โข (๐ฅ โ โ โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ๐น) |
5 | 4 | adantl 483 |
. . . . . . . 8
โข ((ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ โง ๐ฅ โ โ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ๐น) |
6 | 1 | pjfi 30688 |
. . . . . . . . . . . . 13
โข
(projโโ๐น): โโถ โ |
7 | 2 | pjfi 30688 |
. . . . . . . . . . . . 13
โข
(projโโ๐บ): โโถ โ |
8 | 6, 7 | hocofi 30750 |
. . . . . . . . . . . 12
โข
((projโโ๐น) โ
(projโโ๐บ)): โโถ โ |
9 | 3 | pjfi 30688 |
. . . . . . . . . . . 12
โข
(projโโ๐ป): โโถ โ |
10 | 8, 9 | hocofni 30751 |
. . . . . . . . . . 11
โข
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) Fn โ |
11 | | fnfvelrn 7036 |
. . . . . . . . . . 11
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) Fn โ โง ๐ฅ โ โ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))) |
12 | 10, 11 | mpan 689 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))) |
13 | | ssel 3942 |
. . . . . . . . . 10
โข (ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ๐บ)) |
14 | 12, 13 | syl5 34 |
. . . . . . . . 9
โข (ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ โ (๐ฅ โ โ โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ๐บ)) |
15 | 14 | imp 408 |
. . . . . . . 8
โข ((ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ โง ๐ฅ โ โ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ๐บ) |
16 | 5, 15 | elind 4159 |
. . . . . . 7
โข ((ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ โง ๐ฅ โ โ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ (๐น โฉ ๐บ)) |
17 | 16 | adantll 713 |
. . . . . 6
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ (๐น โฉ ๐บ)) |
18 | 3, 2, 1 | pj2cocli 31189 |
. . . . . . . . 9
โข (๐ฅ โ โ โ
((((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น))โ๐ฅ) โ ๐ป) |
19 | | fveq1 6846 |
. . . . . . . . . 10
โข
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น))โ๐ฅ)) |
20 | 19 | eleq1d 2823 |
. . . . . . . . 9
โข
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป โ
((((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น))โ๐ฅ) โ ๐ป)) |
21 | 18, 20 | syl5ibr 246 |
. . . . . . . 8
โข
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โ (๐ฅ โ โ โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป)) |
22 | 21 | imp 408 |
. . . . . . 7
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ๐ฅ โ โ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป) |
23 | 22 | adantlr 714 |
. . . . . 6
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ๐ป) |
24 | 17, 23 | elind 4159 |
. . . . 5
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ((๐น โฉ ๐บ) โฉ ๐ป)) |
25 | 8, 9 | hococli 30749 |
. . . . . . . 8
โข (๐ฅ โ โ โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ) |
26 | | hvsubcl 30001 |
. . . . . . . 8
โข ((๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ) โ (๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) โ โ) |
27 | 25, 26 | mpdan 686 |
. . . . . . 7
โข (๐ฅ โ โ โ (๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) โ โ) |
28 | 27 | adantl 483 |
. . . . . 6
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ (๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) โ โ) |
29 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)) โ ๐ฅ โ โ) |
30 | 25 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ) |
31 | 1, 2 | chincli 30444 |
. . . . . . . . . . . . . . 15
โข (๐น โฉ ๐บ) โ
Cโ |
32 | 31, 3 | chincli 30444 |
. . . . . . . . . . . . . 14
โข ((๐น โฉ ๐บ) โฉ ๐ป) โ
Cโ |
33 | 32 | cheli 30216 |
. . . . . . . . . . . . 13
โข (๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป) โ ๐ฆ โ โ) |
34 | 33 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)) โ ๐ฆ โ โ) |
35 | 29, 30, 34 | 3jca 1129 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)) โ (๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ)) |
36 | 35 | adantl 483 |
. . . . . . . . . 10
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง (๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป))) โ (๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ)) |
37 | | his2sub 30076 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ) โ ((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = ((๐ฅ ยทih ๐ฆ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ))) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง (๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป))) โ ((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = ((๐ฅ ยทih ๐ฆ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ))) |
39 | 19 | adantr 482 |
. . . . . . . . . . . 12
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น))โ๐ฅ)) |
40 | 39 | oveq1d 7377 |
. . . . . . . . . . 11
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) =
(((((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น))โ๐ฅ) ยทih ๐ฆ)) |
41 | 3, 2, 1 | pjadj2coi 31188 |
. . . . . . . . . . . . 13
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
(((((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ))) |
42 | 33, 41 | sylan2 594 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)) โ
(((((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ))) |
43 | 1, 2, 3 | pj3lem1 31190 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ) = ๐ฆ) |
44 | 43 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข (๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป) โ (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) |
45 | 44 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)) โ (๐ฅ ยทih
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฆ)) = (๐ฅ ยทih ๐ฆ)) |
46 | 42, 45 | eqtrd 2777 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)) โ
(((((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih ๐ฆ)) |
47 | 40, 46 | sylan9eq 2797 |
. . . . . . . . . 10
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง (๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป))) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) = (๐ฅ ยทih ๐ฆ)) |
48 | 47 | oveq1d 7377 |
. . . . . . . . 9
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง (๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป))) โ
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ)) = ((๐ฅ ยทih ๐ฆ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ))) |
49 | 25, 33 | anim12i 614 |
. . . . . . . . . . . 12
โข ((๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ)) |
50 | 49 | adantl 483 |
. . . . . . . . . . 11
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง (๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป))) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ)) |
51 | | hicl 30064 |
. . . . . . . . . . 11
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฆ โ โ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
โ) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง (๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป))) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
โ) |
53 | 52 | subidd 11507 |
. . . . . . . . 9
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง (๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป))) โ
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) ยทih ๐ฆ)) = 0) |
54 | 38, 48, 53 | 3eqtr2d 2783 |
. . . . . . . 8
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง (๐ฅ โ โ โง ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป))) โ ((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0) |
55 | 54 | expr 458 |
. . . . . . 7
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ (๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป) โ ((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0)) |
56 | 55 | ralrimiv 3143 |
. . . . . 6
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ โ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0) |
57 | 32 | chshii 30211 |
. . . . . . 7
โข ((๐น โฉ ๐บ) โฉ ๐ป) โ
Sโ |
58 | | shocel 30266 |
. . . . . . 7
โข (((๐น โฉ ๐บ) โฉ ๐ป) โ Sโ
โ ((๐ฅ
โโ ((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) โ (โฅโ((๐น โฉ ๐บ) โฉ ๐ป)) โ ((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) โ โ โง โ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0))) |
59 | 57, 58 | ax-mp 5 |
. . . . . 6
โข ((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) โ (โฅโ((๐น โฉ ๐บ) โฉ ๐ป)) โ ((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) โ โ โง โ๐ฆ โ ((๐น โฉ ๐บ) โฉ ๐ป)((๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) ยทih ๐ฆ) = 0)) |
60 | 28, 56, 59 | sylanbrc 584 |
. . . . 5
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ (๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) โ (โฅโ((๐น โฉ ๐บ) โฉ ๐ป))) |
61 | 32 | pjvi 30689 |
. . . . 5
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ ((๐น โฉ ๐บ) โฉ ๐ป) โง (๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) โ (โฅโ((๐น โฉ ๐บ) โฉ ๐ป))) โ
((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ(((((projโโ๐น) โ
(projโโ๐บ)) โ (projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
((((projโโ๐น) โ (projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)))) = ((((projโโ๐น) โ
(projโโ๐บ)) โ (projโโ๐ป))โ๐ฅ)) |
62 | 24, 60, 61 | syl2anc 585 |
. . . 4
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ
((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ(((((projโโ๐น) โ
(projโโ๐บ)) โ (projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
((((projโโ๐น) โ (projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)))) = ((((projโโ๐น) โ
(projโโ๐บ)) โ (projโโ๐ป))โ๐ฅ)) |
63 | | id 22 |
. . . . . . . 8
โข (๐ฅ โ โ โ ๐ฅ โ
โ) |
64 | | hvaddsub12 30022 |
. . . . . . . 8
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ โง ๐ฅ โ โ โง
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ) โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ))) = (๐ฅ +โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)))) |
65 | 25, 63, 25, 64 | syl3anc 1372 |
. . . . . . 7
โข (๐ฅ โ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ))) = (๐ฅ +โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)))) |
66 | | hvsubid 30010 |
. . . . . . . . . 10
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) = 0โ) |
67 | 25, 66 | syl 17 |
. . . . . . . . 9
โข (๐ฅ โ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)) = 0โ) |
68 | 67 | oveq2d 7378 |
. . . . . . . 8
โข (๐ฅ โ โ โ (๐ฅ +โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ))) = (๐ฅ +โ
0โ)) |
69 | | ax-hvaddid 29988 |
. . . . . . . 8
โข (๐ฅ โ โ โ (๐ฅ +โ
0โ) = ๐ฅ) |
70 | 68, 69 | eqtrd 2777 |
. . . . . . 7
โข (๐ฅ โ โ โ (๐ฅ +โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ))) = ๐ฅ) |
71 | 65, 70 | eqtrd 2777 |
. . . . . 6
โข (๐ฅ โ โ โ
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ))) = ๐ฅ) |
72 | 71 | fveq2d 6851 |
. . . . 5
โข (๐ฅ โ โ โ
((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ(((((projโโ๐น) โ
(projโโ๐บ)) โ (projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
((((projโโ๐น) โ (projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)))) = ((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ)) |
73 | 72 | adantl 483 |
. . . 4
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ
((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ(((((projโโ๐น) โ
(projโโ๐บ)) โ (projโโ๐ป))โ๐ฅ) +โ (๐ฅ โโ
((((projโโ๐น) โ (projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ)))) = ((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ)) |
74 | 62, 73 | eqtr3d 2779 |
. . 3
โข
((((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โง ๐ฅ โ โ) โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ)) |
75 | 74 | ralrimiva 3144 |
. 2
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โ โ๐ฅ โ โ
((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ)) |
76 | 8, 9 | hocofi 30750 |
. . 3
โข
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)): โโถ โ |
77 | 32 | pjfi 30688 |
. . 3
โข
(projโโ((๐น โฉ ๐บ) โฉ ๐ป)): โโถ โ |
78 | 76, 77 | hoeqi 30745 |
. 2
โข
(โ๐ฅ โ
โ ((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป))โ๐ฅ) = ((projโโ((๐น โฉ ๐บ) โฉ ๐ป))โ๐ฅ) โ
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (projโโ((๐น โฉ ๐บ) โฉ ๐ป))) |
79 | 75, 78 | sylib 217 |
1
โข
(((((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (((projโโ๐ป) โ
(projโโ๐บ)) โ
(projโโ๐น)) โง ran
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) โ ๐บ) โ
(((projโโ๐น) โ
(projโโ๐บ)) โ
(projโโ๐ป)) = (projโโ((๐น โฉ ๐บ) โฉ ๐ป))) |