Step | Hyp | Ref
| Expression |
1 | | elin 3925 |
. . . . . . . 8
โข (๐ฅ โ (๐ โฉ ๐) โ (๐ฅ โ ๐ โง ๐ฅ โ ๐)) |
2 | | mayete3.a |
. . . . . . . . . . . . 13
โข ๐ด โ
Cโ |
3 | | mayete3.c |
. . . . . . . . . . . . 13
โข ๐ถ โ
Cโ |
4 | 2, 3 | chjcli 30198 |
. . . . . . . . . . . 12
โข (๐ด โจโ ๐ถ) โ
Cโ |
5 | | mayete3.f |
. . . . . . . . . . . 12
โข ๐น โ
Cโ |
6 | 4, 5 | chjcli 30198 |
. . . . . . . . . . 11
โข ((๐ด โจโ ๐ถ) โจโ ๐น) โ
Cโ |
7 | 6 | cheli 29973 |
. . . . . . . . . 10
โข (๐ฅ โ ((๐ด โจโ ๐ถ) โจโ ๐น) โ ๐ฅ โ โ) |
8 | | mayete3.x |
. . . . . . . . . 10
โข ๐ = ((๐ด โจโ ๐ถ) โจโ ๐น) |
9 | 7, 8 | eleq2s 2857 |
. . . . . . . . 9
โข (๐ฅ โ ๐ โ ๐ฅ โ โ) |
10 | 9 | adantr 482 |
. . . . . . . 8
โข ((๐ฅ โ ๐ โง ๐ฅ โ ๐) โ ๐ฅ โ โ) |
11 | 1, 10 | sylbi 216 |
. . . . . . 7
โข (๐ฅ โ (๐ โฉ ๐) โ ๐ฅ โ โ) |
12 | | ax-hvmulid 29747 |
. . . . . . . 8
โข (๐ฅ โ โ โ (1
ยทโ ๐ฅ) = ๐ฅ) |
13 | | 2cn 12162 |
. . . . . . . . . . 11
โข 2 โ
โ |
14 | | 2ne0 12191 |
. . . . . . . . . . 11
โข 2 โ
0 |
15 | | recid2 11762 |
. . . . . . . . . . 11
โข ((2
โ โ โง 2 โ 0) โ ((1 / 2) ยท 2) =
1) |
16 | 13, 14, 15 | mp2an 691 |
. . . . . . . . . 10
โข ((1 / 2)
ยท 2) = 1 |
17 | 16 | oveq1i 7360 |
. . . . . . . . 9
โข (((1 / 2)
ยท 2) ยทโ ๐ฅ) = (1 ยทโ
๐ฅ) |
18 | | halfcn 12302 |
. . . . . . . . . 10
โข (1 / 2)
โ โ |
19 | | ax-hvmulass 29748 |
. . . . . . . . . 10
โข (((1 / 2)
โ โ โง 2 โ โ โง ๐ฅ โ โ) โ (((1 / 2) ยท 2)
ยทโ ๐ฅ) = ((1 / 2)
ยทโ (2 ยทโ ๐ฅ))) |
20 | 18, 13, 19 | mp3an12 1452 |
. . . . . . . . 9
โข (๐ฅ โ โ โ (((1 / 2)
ยท 2) ยทโ ๐ฅ) = ((1 / 2)
ยทโ (2 ยทโ ๐ฅ))) |
21 | 17, 20 | eqtr3id 2792 |
. . . . . . . 8
โข (๐ฅ โ โ โ (1
ยทโ ๐ฅ) = ((1 / 2)
ยทโ (2 ยทโ ๐ฅ))) |
22 | 12, 21 | eqtr3d 2780 |
. . . . . . 7
โข (๐ฅ โ โ โ ๐ฅ = ((1 / 2)
ยทโ (2 ยทโ ๐ฅ))) |
23 | 11, 22 | syl 17 |
. . . . . 6
โข (๐ฅ โ (๐ โฉ ๐) โ ๐ฅ = ((1 / 2)
ยทโ (2 ยทโ ๐ฅ))) |
24 | | hv2times 29802 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ (2
ยทโ ๐ฅ) = (๐ฅ +โ ๐ฅ)) |
25 | 24 | oveq1d 7365 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ ((2
ยทโ ๐ฅ) +โ ๐ฅ) = ((๐ฅ +โ ๐ฅ) +โ ๐ฅ)) |
26 | 11, 25 | syl 17 |
. . . . . . . . . . . 12
โข (๐ฅ โ (๐ โฉ ๐) โ ((2
ยทโ ๐ฅ) +โ ๐ฅ) = ((๐ฅ +โ ๐ฅ) +โ ๐ฅ)) |
27 | | inss2 4188 |
. . . . . . . . . . . . . 14
โข (๐ โฉ ๐) โ ๐ |
28 | 27 | sseli 3939 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (๐ โฉ ๐) โ ๐ฅ โ ๐) |
29 | | mayete3.y |
. . . . . . . . . . . . . . 15
โข ๐ = (((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โฉ (๐น โจโ ๐บ)) |
30 | 29 | elin2 4156 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ ๐ โ (๐ฅ โ ((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โง ๐ฅ โ (๐น โจโ ๐บ))) |
31 | | elin 3925 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ ((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โ (๐ฅ โ (๐ด โจโ ๐ต) โง ๐ฅ โ (๐ถ โจโ ๐ท))) |
32 | | mayete3.ab |
. . . . . . . . . . . . . . . . . . 19
โข ๐ด โ (โฅโ๐ต) |
33 | | mayete3.b |
. . . . . . . . . . . . . . . . . . . 20
โข ๐ต โ
Cโ |
34 | 2, 33 | pjdsi 30453 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฅ โ (๐ด โจโ ๐ต) โง ๐ด โ (โฅโ๐ต)) โ ๐ฅ = (((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ต)โ๐ฅ))) |
35 | 32, 34 | mpan2 690 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ (๐ด โจโ ๐ต) โ ๐ฅ = (((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ต)โ๐ฅ))) |
36 | | mayete3.cd |
. . . . . . . . . . . . . . . . . . 19
โข ๐ถ โ (โฅโ๐ท) |
37 | | mayete3.d |
. . . . . . . . . . . . . . . . . . . 20
โข ๐ท โ
Cโ |
38 | 3, 37 | pjdsi 30453 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฅ โ (๐ถ โจโ ๐ท) โง ๐ถ โ (โฅโ๐ท)) โ ๐ฅ = (((projโโ๐ถ)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) |
39 | 36, 38 | mpan2 690 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ (๐ถ โจโ ๐ท) โ ๐ฅ = (((projโโ๐ถ)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) |
40 | 35, 39 | oveqan12d 7369 |
. . . . . . . . . . . . . . . . 17
โข ((๐ฅ โ (๐ด โจโ ๐ต) โง ๐ฅ โ (๐ถ โจโ ๐ท)) โ (๐ฅ +โ ๐ฅ) = ((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ต)โ๐ฅ)) +โ
(((projโโ๐ถ)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)))) |
41 | 31, 40 | sylbi 216 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ ((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โ (๐ฅ +โ ๐ฅ) = ((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ต)โ๐ฅ)) +โ
(((projโโ๐ถ)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)))) |
42 | | inss1 4187 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โ (๐ด โจโ ๐ต) |
43 | 42 | sseli 3939 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ ((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โ ๐ฅ โ (๐ด โจโ ๐ต)) |
44 | 2, 33 | chjcli 30198 |
. . . . . . . . . . . . . . . . . 18
โข (๐ด โจโ ๐ต) โ
Cโ |
45 | 44 | cheli 29973 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ (๐ด โจโ ๐ต) โ ๐ฅ โ โ) |
46 | 2 | pjhcli 30159 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ
((projโโ๐ด)โ๐ฅ) โ โ) |
47 | 33 | pjhcli 30159 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ
((projโโ๐ต)โ๐ฅ) โ โ) |
48 | 3 | pjhcli 30159 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ
((projโโ๐ถ)โ๐ฅ) โ โ) |
49 | 37 | pjhcli 30159 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ โ โ
((projโโ๐ท)โ๐ฅ) โ โ) |
50 | | hvadd4 29777 |
. . . . . . . . . . . . . . . . . 18
โข
(((((projโโ๐ด)โ๐ฅ) โ โ โง
((projโโ๐ต)โ๐ฅ) โ โ) โง
(((projโโ๐ถ)โ๐ฅ) โ โ โง
((projโโ๐ท)โ๐ฅ) โ โ)) โ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ต)โ๐ฅ)) +โ
(((projโโ๐ถ)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) = ((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)))) |
51 | 46, 47, 48, 49, 50 | syl22anc 838 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ โ โ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ต)โ๐ฅ)) +โ
(((projโโ๐ถ)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) = ((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)))) |
52 | 43, 45, 51 | 3syl 18 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ ((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ต)โ๐ฅ)) +โ
(((projโโ๐ถ)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) = ((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)))) |
53 | 41, 52 | eqtrd 2778 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ ((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โ (๐ฅ +โ ๐ฅ) = ((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)))) |
54 | | mayete3.fg |
. . . . . . . . . . . . . . . 16
โข ๐น โ (โฅโ๐บ) |
55 | | mayete3.g |
. . . . . . . . . . . . . . . . 17
โข ๐บ โ
Cโ |
56 | 5, 55 | pjdsi 30453 |
. . . . . . . . . . . . . . . 16
โข ((๐ฅ โ (๐น โจโ ๐บ) โง ๐น โ (โฅโ๐บ)) โ ๐ฅ = (((projโโ๐น)โ๐ฅ) +โ
((projโโ๐บ)โ๐ฅ))) |
57 | 54, 56 | mpan2 690 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ (๐น โจโ ๐บ) โ ๐ฅ = (((projโโ๐น)โ๐ฅ) +โ
((projโโ๐บ)โ๐ฅ))) |
58 | 53, 57 | oveqan12d 7369 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ ((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โง ๐ฅ โ (๐น โจโ ๐บ)) โ ((๐ฅ +โ ๐ฅ) +โ ๐ฅ) = (((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) +โ
(((projโโ๐น)โ๐ฅ) +โ
((projโโ๐บ)โ๐ฅ)))) |
59 | 30, 58 | sylbi 216 |
. . . . . . . . . . . . 13
โข (๐ฅ โ ๐ โ ((๐ฅ +โ ๐ฅ) +โ ๐ฅ) = (((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) +โ
(((projโโ๐น)โ๐ฅ) +โ
((projโโ๐บ)โ๐ฅ)))) |
60 | 28, 59 | syl 17 |
. . . . . . . . . . . 12
โข (๐ฅ โ (๐ โฉ ๐) โ ((๐ฅ +โ ๐ฅ) +โ ๐ฅ) = (((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) +โ
(((projโโ๐น)โ๐ฅ) +โ
((projโโ๐บ)โ๐ฅ)))) |
61 | | hvaddcl 29753 |
. . . . . . . . . . . . . . 15
โข
((((projโโ๐ด)โ๐ฅ) โ โ โง
((projโโ๐ถ)โ๐ฅ) โ โ) โ
(((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) โ โ) |
62 | 46, 48, 61 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ
(((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) โ โ) |
63 | | hvaddcl 29753 |
. . . . . . . . . . . . . . 15
โข
((((projโโ๐ต)โ๐ฅ) โ โ โง
((projโโ๐ท)โ๐ฅ) โ โ) โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) โ โ) |
64 | 47, 49, 63 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) โ โ) |
65 | 5 | pjhcli 30159 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ
((projโโ๐น)โ๐ฅ) โ โ) |
66 | 55 | pjhcli 30159 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ
((projโโ๐บ)โ๐ฅ) โ โ) |
67 | | hvadd4 29777 |
. . . . . . . . . . . . . 14
โข
((((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) โ โ โง
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) โ โ) โง
(((projโโ๐น)โ๐ฅ) โ โ โง
((projโโ๐บ)โ๐ฅ) โ โ)) โ
(((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) +โ
(((projโโ๐น)โ๐ฅ) +โ
((projโโ๐บ)โ๐ฅ))) =
(((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) +โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)))) |
68 | 62, 64, 65, 66, 67 | syl22anc 838 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ
(((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) +โ
(((projโโ๐น)โ๐ฅ) +โ
((projโโ๐บ)โ๐ฅ))) =
(((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) +โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)))) |
69 | 11, 68 | syl 17 |
. . . . . . . . . . . 12
โข (๐ฅ โ (๐ โฉ ๐) โ
(((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ))) +โ
(((projโโ๐น)โ๐ฅ) +โ
((projโโ๐บ)โ๐ฅ))) =
(((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) +โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)))) |
70 | 26, 60, 69 | 3eqtrd 2782 |
. . . . . . . . . . 11
โข (๐ฅ โ (๐ โฉ ๐) โ ((2
ยทโ ๐ฅ) +โ ๐ฅ) = (((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) +โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)))) |
71 | | inss1 4187 |
. . . . . . . . . . . . . 14
โข (๐ โฉ ๐) โ ๐ |
72 | 71 | sseli 3939 |
. . . . . . . . . . . . 13
โข (๐ฅ โ (๐ โฉ ๐) โ ๐ฅ โ ๐) |
73 | 72, 8 | eleqtrdi 2849 |
. . . . . . . . . . . 12
โข (๐ฅ โ (๐ โฉ ๐) โ ๐ฅ โ ((๐ด โจโ ๐ถ) โจโ ๐น)) |
74 | | mayete3.ac |
. . . . . . . . . . . 12
โข ๐ด โ (โฅโ๐ถ) |
75 | | mayete3.af |
. . . . . . . . . . . . 13
โข ๐ด โ (โฅโ๐น) |
76 | | mayete3.cf |
. . . . . . . . . . . . 13
โข ๐ถ โ (โฅโ๐น) |
77 | 2, 3, 5 | pjds3i 30454 |
. . . . . . . . . . . . 13
โข (((๐ฅ โ ((๐ด โจโ ๐ถ) โจโ ๐น) โง ๐ด โ (โฅโ๐ถ)) โง (๐ด โ (โฅโ๐น) โง ๐ถ โ (โฅโ๐น))) โ ๐ฅ = ((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ))) |
78 | 75, 76, 77 | mpanr12 704 |
. . . . . . . . . . . 12
โข ((๐ฅ โ ((๐ด โจโ ๐ถ) โจโ ๐น) โง ๐ด โ (โฅโ๐ถ)) โ ๐ฅ = ((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ))) |
79 | 73, 74, 78 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ฅ โ (๐ โฉ ๐) โ ๐ฅ = ((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ))) |
80 | 70, 79 | oveq12d 7368 |
. . . . . . . . . 10
โข (๐ฅ โ (๐ โฉ ๐) โ (((2
ยทโ ๐ฅ) +โ ๐ฅ) โโ ๐ฅ) =
((((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) +โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ))) โโ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)))) |
81 | | hvmulcl 29754 |
. . . . . . . . . . . . 13
โข ((2
โ โ โง ๐ฅ
โ โ) โ (2 ยทโ ๐ฅ) โ โ) |
82 | 13, 81 | mpan 689 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ (2
ยทโ ๐ฅ) โ โ) |
83 | | hvpncan 29780 |
. . . . . . . . . . . 12
โข (((2
ยทโ ๐ฅ) โ โ โง ๐ฅ โ โ) โ (((2
ยทโ ๐ฅ) +โ ๐ฅ) โโ ๐ฅ) = (2
ยทโ ๐ฅ)) |
84 | 82, 83 | mpancom 687 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ (((2
ยทโ ๐ฅ) +โ ๐ฅ) โโ ๐ฅ) = (2
ยทโ ๐ฅ)) |
85 | 11, 84 | syl 17 |
. . . . . . . . . 10
โข (๐ฅ โ (๐ โฉ ๐) โ (((2
ยทโ ๐ฅ) +โ ๐ฅ) โโ ๐ฅ) = (2
ยทโ ๐ฅ)) |
86 | 80, 85 | eqtr3d 2780 |
. . . . . . . . 9
โข (๐ฅ โ (๐ โฉ ๐) โ
((((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) +โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ))) โโ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ))) = (2 ยทโ
๐ฅ)) |
87 | | hvaddcl 29753 |
. . . . . . . . . . . 12
โข
(((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) โ โ โง
((projโโ๐น)โ๐ฅ) โ โ) โ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) โ โ) |
88 | 62, 65, 87 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) โ โ) |
89 | | hvaddcl 29753 |
. . . . . . . . . . . 12
โข
(((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) โ โ โง
((projโโ๐บ)โ๐ฅ) โ โ) โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)) โ โ) |
90 | 64, 66, 89 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)) โ โ) |
91 | | hvpncan2 29781 |
. . . . . . . . . . 11
โข
((((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) โ โ โง
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)) โ โ) โ
((((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) +โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ))) โโ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ))) = ((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ))) |
92 | 88, 90, 91 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
((((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) +โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ))) โโ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ))) = ((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ))) |
93 | 11, 92 | syl 17 |
. . . . . . . . 9
โข (๐ฅ โ (๐ โฉ ๐) โ
((((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ)) +โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ))) โโ
((((projโโ๐ด)โ๐ฅ) +โ
((projโโ๐ถ)โ๐ฅ)) +โ
((projโโ๐น)โ๐ฅ))) = ((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ))) |
94 | 86, 93 | eqtr3d 2780 |
. . . . . . . 8
โข (๐ฅ โ (๐ โฉ ๐) โ (2
ยทโ ๐ฅ) = ((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ))) |
95 | 33 | pjcli 30158 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
((projโโ๐ต)โ๐ฅ) โ ๐ต) |
96 | 37 | pjcli 30158 |
. . . . . . . . . . 11
โข (๐ฅ โ โ โ
((projโโ๐ท)โ๐ฅ) โ ๐ท) |
97 | 33 | chshii 29968 |
. . . . . . . . . . . 12
โข ๐ต โ
Sโ |
98 | 37 | chshii 29968 |
. . . . . . . . . . . 12
โข ๐ท โ
Sโ |
99 | 97, 98 | shsvai 30105 |
. . . . . . . . . . 11
โข
((((projโโ๐ต)โ๐ฅ) โ ๐ต โง ((projโโ๐ท)โ๐ฅ) โ ๐ท) โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) โ (๐ต +โ ๐ท)) |
100 | 95, 96, 99 | syl2anc 585 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
(((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) โ (๐ต +โ ๐ท)) |
101 | 55 | pjcli 30158 |
. . . . . . . . . 10
โข (๐ฅ โ โ โ
((projโโ๐บ)โ๐ฅ) โ ๐บ) |
102 | 97, 98 | shscli 30058 |
. . . . . . . . . . 11
โข (๐ต +โ ๐ท) โ
Sโ |
103 | 55 | chshii 29968 |
. . . . . . . . . . 11
โข ๐บ โ
Sโ |
104 | 102, 103 | shsvai 30105 |
. . . . . . . . . 10
โข
(((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) โ (๐ต +โ ๐ท) โง
((projโโ๐บ)โ๐ฅ) โ ๐บ) โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)) โ ((๐ต +โ ๐ท) +โ ๐บ)) |
105 | 100, 101,
104 | syl2anc 585 |
. . . . . . . . 9
โข (๐ฅ โ โ โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)) โ ((๐ต +โ ๐ท) +โ ๐บ)) |
106 | 11, 105 | syl 17 |
. . . . . . . 8
โข (๐ฅ โ (๐ โฉ ๐) โ
((((projโโ๐ต)โ๐ฅ) +โ
((projโโ๐ท)โ๐ฅ)) +โ
((projโโ๐บ)โ๐ฅ)) โ ((๐ต +โ ๐ท) +โ ๐บ)) |
107 | 94, 106 | eqeltrd 2839 |
. . . . . . 7
โข (๐ฅ โ (๐ โฉ ๐) โ (2
ยทโ ๐ฅ) โ ((๐ต +โ ๐ท) +โ ๐บ)) |
108 | 102, 103 | shscli 30058 |
. . . . . . . 8
โข ((๐ต +โ ๐ท) +โ ๐บ) โ
Sโ |
109 | | shmulcl 29959 |
. . . . . . . 8
โข ((((๐ต +โ ๐ท) +โ ๐บ) โ
Sโ โง (1 / 2) โ โ โง (2
ยทโ ๐ฅ) โ ((๐ต +โ ๐ท) +โ ๐บ)) โ ((1 / 2)
ยทโ (2 ยทโ ๐ฅ)) โ ((๐ต +โ ๐ท) +โ ๐บ)) |
110 | 108, 18, 109 | mp3an12 1452 |
. . . . . . 7
โข ((2
ยทโ ๐ฅ) โ ((๐ต +โ ๐ท) +โ ๐บ) โ ((1 / 2)
ยทโ (2 ยทโ ๐ฅ)) โ ((๐ต +โ ๐ท) +โ ๐บ)) |
111 | 107, 110 | syl 17 |
. . . . . 6
โข (๐ฅ โ (๐ โฉ ๐) โ ((1 / 2)
ยทโ (2 ยทโ ๐ฅ)) โ ((๐ต +โ ๐ท) +โ ๐บ)) |
112 | 23, 111 | eqeltrd 2839 |
. . . . 5
โข (๐ฅ โ (๐ โฉ ๐) โ ๐ฅ โ ((๐ต +โ ๐ท) +โ ๐บ)) |
113 | 112 | ssriv 3947 |
. . . 4
โข (๐ โฉ ๐) โ ((๐ต +โ ๐ท) +โ ๐บ) |
114 | 33, 37 | chsleji 30199 |
. . . . 5
โข (๐ต +โ ๐ท) โ (๐ต โจโ ๐ท) |
115 | 33, 37 | chjcli 30198 |
. . . . . . 7
โข (๐ต โจโ ๐ท) โ
Cโ |
116 | 115 | chshii 29968 |
. . . . . 6
โข (๐ต โจโ ๐ท) โ
Sโ |
117 | 102, 116,
103 | shlessi 30118 |
. . . . 5
โข ((๐ต +โ ๐ท) โ (๐ต โจโ ๐ท) โ ((๐ต +โ ๐ท) +โ ๐บ) โ ((๐ต โจโ ๐ท) +โ ๐บ)) |
118 | 114, 117 | ax-mp 5 |
. . . 4
โข ((๐ต +โ ๐ท) +โ ๐บ) โ ((๐ต โจโ ๐ท) +โ ๐บ) |
119 | 113, 118 | sstri 3952 |
. . 3
โข (๐ โฉ ๐) โ ((๐ต โจโ ๐ท) +โ ๐บ) |
120 | 115, 55 | chsleji 30199 |
. . 3
โข ((๐ต โจโ ๐ท) +โ ๐บ) โ ((๐ต โจโ ๐ท) โจโ ๐บ) |
121 | 119, 120 | sstri 3952 |
. 2
โข (๐ โฉ ๐) โ ((๐ต โจโ ๐ท) โจโ ๐บ) |
122 | | mayete3.z |
. 2
โข ๐ = ((๐ต โจโ ๐ท) โจโ ๐บ) |
123 | 121, 122 | sseqtrri 3980 |
1
โข (๐ โฉ ๐) โ ๐ |