Step | Hyp | Ref
| Expression |
1 | | hstcl 31201 |
. . . . . . . 8
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ (๐โ๐ด) โ โ) |
2 | | choccl 30290 |
. . . . . . . . 9
โข (๐ด โ
Cโ โ (โฅโ๐ด) โ Cโ
) |
3 | | hstcl 31201 |
. . . . . . . . 9
โข ((๐ โ CHStates โง
(โฅโ๐ด) โ
Cโ ) โ (๐โ(โฅโ๐ด)) โ โ) |
4 | 2, 3 | sylan2 594 |
. . . . . . . 8
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ (๐โ(โฅโ๐ด)) โ โ) |
5 | | his7 30074 |
. . . . . . . 8
โข (((๐โ๐ด) โ โ โง (๐โ๐ด) โ โ โง (๐โ(โฅโ๐ด)) โ โ) โ ((๐โ๐ด) ยทih
((๐โ๐ด) +โ (๐โ(โฅโ๐ด)))) = (((๐โ๐ด) ยทih (๐โ๐ด)) + ((๐โ๐ด) ยทih (๐โ(โฅโ๐ด))))) |
6 | 1, 1, 4, 5 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ ((๐โ๐ด) ยทih
((๐โ๐ด) +โ (๐โ(โฅโ๐ด)))) = (((๐โ๐ด) ยทih (๐โ๐ด)) + ((๐โ๐ด) ยทih (๐โ(โฅโ๐ด))))) |
7 | | normsq 30118 |
. . . . . . . . . 10
โข ((๐โ๐ด) โ โ โ
((normโโ(๐โ๐ด))โ2) = ((๐โ๐ด) ยทih (๐โ๐ด))) |
8 | 1, 7 | syl 17 |
. . . . . . . . 9
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
((normโโ(๐โ๐ด))โ2) = ((๐โ๐ด) ยทih (๐โ๐ด))) |
9 | 8 | eqcomd 2743 |
. . . . . . . 8
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ ((๐โ๐ด) ยทih (๐โ๐ด)) = ((normโโ(๐โ๐ด))โ2)) |
10 | | ococ 30390 |
. . . . . . . . . . . 12
โข (๐ด โ
Cโ โ (โฅโ(โฅโ๐ด)) = ๐ด) |
11 | | eqimss2 4006 |
. . . . . . . . . . . 12
โข
((โฅโ(โฅโ๐ด)) = ๐ด โ ๐ด โ (โฅโ(โฅโ๐ด))) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
โข (๐ด โ
Cโ โ ๐ด โ (โฅโ(โฅโ๐ด))) |
13 | 2, 12 | jca 513 |
. . . . . . . . . 10
โข (๐ด โ
Cโ โ ((โฅโ๐ด) โ Cโ
โง ๐ด โ
(โฅโ(โฅโ๐ด)))) |
14 | 13 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ ((โฅโ๐ด) โ Cโ
โง ๐ด โ
(โฅโ(โฅโ๐ด)))) |
15 | | hstorth 31204 |
. . . . . . . . 9
โข (((๐ โ CHStates โง ๐ด โ
Cโ ) โง ((โฅโ๐ด) โ Cโ
โง ๐ด โ
(โฅโ(โฅโ๐ด)))) โ ((๐โ๐ด) ยทih (๐โ(โฅโ๐ด))) = 0) |
16 | 14, 15 | mpdan 686 |
. . . . . . . 8
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ ((๐โ๐ด) ยทih (๐โ(โฅโ๐ด))) = 0) |
17 | 9, 16 | oveq12d 7380 |
. . . . . . 7
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ (((๐โ๐ด) ยทih (๐โ๐ด)) + ((๐โ๐ด) ยทih (๐โ(โฅโ๐ด)))) =
(((normโโ(๐โ๐ด))โ2) + 0)) |
18 | | normcl 30109 |
. . . . . . . . . . 11
โข ((๐โ๐ด) โ โ โ
(normโโ(๐โ๐ด)) โ โ) |
19 | 1, 18 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
(normโโ(๐โ๐ด)) โ โ) |
20 | 19 | resqcld 14037 |
. . . . . . . . 9
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
((normโโ(๐โ๐ด))โ2) โ โ) |
21 | 20 | recnd 11190 |
. . . . . . . 8
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
((normโโ(๐โ๐ด))โ2) โ โ) |
22 | 21 | addid1d 11362 |
. . . . . . 7
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
(((normโโ(๐โ๐ด))โ2) + 0) =
((normโโ(๐โ๐ด))โ2)) |
23 | 6, 17, 22 | 3eqtrrd 2782 |
. . . . . 6
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
((normโโ(๐โ๐ด))โ2) = ((๐โ๐ด) ยทih
((๐โ๐ด) +โ (๐โ(โฅโ๐ด))))) |
24 | | hstoc 31206 |
. . . . . . 7
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ ((๐โ๐ด) +โ (๐โ(โฅโ๐ด))) = (๐โ โ)) |
25 | 24 | oveq2d 7378 |
. . . . . 6
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ ((๐โ๐ด) ยทih
((๐โ๐ด) +โ (๐โ(โฅโ๐ด)))) = ((๐โ๐ด) ยทih (๐โ
โ))) |
26 | 23, 25 | eqtrd 2777 |
. . . . 5
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
((normโโ(๐โ๐ด))โ2) = ((๐โ๐ด) ยทih (๐โ
โ))) |
27 | | id 22 |
. . . . 5
โข (((๐โ๐ด) ยทih (๐โ โ)) = 0 โ
((๐โ๐ด) ยทih (๐โ โ)) =
0) |
28 | 26, 27 | sylan9eq 2797 |
. . . 4
โข (((๐ โ CHStates โง ๐ด โ
Cโ ) โง ((๐โ๐ด) ยทih (๐โ โ)) = 0) โ
((normโโ(๐โ๐ด))โ2) = 0) |
29 | 28 | 3impa 1111 |
. . 3
โข ((๐ โ CHStates โง ๐ด โ
Cโ โง ((๐โ๐ด) ยทih (๐โ โ)) = 0) โ
((normโโ(๐โ๐ด))โ2) = 0) |
30 | 19 | recnd 11190 |
. . . . 5
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
(normโโ(๐โ๐ด)) โ โ) |
31 | | sqeq0 14032 |
. . . . 5
โข
((normโโ(๐โ๐ด)) โ โ โ
(((normโโ(๐โ๐ด))โ2) = 0 โ
(normโโ(๐โ๐ด)) = 0)) |
32 | 30, 31 | syl 17 |
. . . 4
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
(((normโโ(๐โ๐ด))โ2) = 0 โ
(normโโ(๐โ๐ด)) = 0)) |
33 | 32 | 3adant3 1133 |
. . 3
โข ((๐ โ CHStates โง ๐ด โ
Cโ โง ((๐โ๐ด) ยทih (๐โ โ)) = 0) โ
(((normโโ(๐โ๐ด))โ2) = 0 โ
(normโโ(๐โ๐ด)) = 0)) |
34 | 29, 33 | mpbid 231 |
. 2
โข ((๐ โ CHStates โง ๐ด โ
Cโ โง ((๐โ๐ด) ยทih (๐โ โ)) = 0) โ
(normโโ(๐โ๐ด)) = 0) |
35 | | hst0h 31212 |
. . 3
โข ((๐ โ CHStates โง ๐ด โ
Cโ ) โ
((normโโ(๐โ๐ด)) = 0 โ (๐โ๐ด) = 0โ)) |
36 | 35 | 3adant3 1133 |
. 2
โข ((๐ โ CHStates โง ๐ด โ
Cโ โง ((๐โ๐ด) ยทih (๐โ โ)) = 0) โ
((normโโ(๐โ๐ด)) = 0 โ (๐โ๐ด) = 0โ)) |
37 | 34, 36 | mpbid 231 |
1
โข ((๐ โ CHStates โง ๐ด โ
Cโ โง ((๐โ๐ด) ยทih (๐โ โ)) = 0) โ
(๐โ๐ด) = 0โ) |