Step | Hyp | Ref
| Expression |
1 | | chst 29947 |
. 2
class
CHStates |
2 | | chba 29903 |
. . . . . . 7
class
โ |
3 | | vf |
. . . . . . . 8
setvar ๐ |
4 | 3 | cv 1541 |
. . . . . . 7
class ๐ |
5 | 2, 4 | cfv 6501 |
. . . . . 6
class (๐โ
โ) |
6 | | cno 29907 |
. . . . . 6
class
normโ |
7 | 5, 6 | cfv 6501 |
. . . . 5
class
(normโโ(๐โ โ)) |
8 | | c1 11059 |
. . . . 5
class
1 |
9 | 7, 8 | wceq 1542 |
. . . 4
wff
(normโโ(๐โ โ)) = 1 |
10 | | vx |
. . . . . . . . 9
setvar ๐ฅ |
11 | 10 | cv 1541 |
. . . . . . . 8
class ๐ฅ |
12 | | vy |
. . . . . . . . . 10
setvar ๐ฆ |
13 | 12 | cv 1541 |
. . . . . . . . 9
class ๐ฆ |
14 | | cort 29914 |
. . . . . . . . 9
class
โฅ |
15 | 13, 14 | cfv 6501 |
. . . . . . . 8
class
(โฅโ๐ฆ) |
16 | 11, 15 | wss 3915 |
. . . . . . 7
wff ๐ฅ โ (โฅโ๐ฆ) |
17 | 11, 4 | cfv 6501 |
. . . . . . . . . 10
class (๐โ๐ฅ) |
18 | 13, 4 | cfv 6501 |
. . . . . . . . . 10
class (๐โ๐ฆ) |
19 | | csp 29906 |
. . . . . . . . . 10
class
ยทih |
20 | 17, 18, 19 | co 7362 |
. . . . . . . . 9
class ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) |
21 | | cc0 11058 |
. . . . . . . . 9
class
0 |
22 | 20, 21 | wceq 1542 |
. . . . . . . 8
wff ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 |
23 | | chj 29917 |
. . . . . . . . . . 11
class
โจโ |
24 | 11, 13, 23 | co 7362 |
. . . . . . . . . 10
class (๐ฅ โจโ ๐ฆ) |
25 | 24, 4 | cfv 6501 |
. . . . . . . . 9
class (๐โ(๐ฅ โจโ ๐ฆ)) |
26 | | cva 29904 |
. . . . . . . . . 10
class
+โ |
27 | 17, 18, 26 | co 7362 |
. . . . . . . . 9
class ((๐โ๐ฅ) +โ (๐โ๐ฆ)) |
28 | 25, 27 | wceq 1542 |
. . . . . . . 8
wff (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)) |
29 | 22, 28 | wa 397 |
. . . . . . 7
wff (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))) |
30 | 16, 29 | wi 4 |
. . . . . 6
wff (๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) |
31 | | cch 29913 |
. . . . . 6
class
Cโ |
32 | 30, 12, 31 | wral 3065 |
. . . . 5
wff
โ๐ฆ โ
Cโ (๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) |
33 | 32, 10, 31 | wral 3065 |
. . . 4
wff
โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) |
34 | 9, 33 | wa 397 |
. . 3
wff
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))) |
35 | | cmap 8772 |
. . . 4
class
โm |
36 | 2, 31, 35 | co 7362 |
. . 3
class ( โ
โm Cโ ) |
37 | 34, 3, 36 | crab 3410 |
. 2
class {๐ โ ( โ
โm Cโ ) โฃ
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))} |
38 | 1, 37 | wceq 1542 |
1
wff CHStates =
{๐ โ ( โ
โm Cโ ) โฃ
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))} |