Step | Hyp | Ref
| Expression |
1 | | ax-hilex 30239 |
. . . 4
โข โ
โ V |
2 | | chex 30466 |
. . . 4
โข
Cโ โ V |
3 | 1, 2 | elmap 8861 |
. . 3
โข (๐ โ ( โ
โm Cโ ) โ ๐: Cโ โถ
โ) |
4 | 3 | anbi1i 624 |
. 2
โข ((๐ โ ( โ
โm Cโ ) โง
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))) โ (๐: Cโ โถ
โ โง ((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))))) |
5 | | fveq1 6887 |
. . . . 5
โข (๐ = ๐ โ (๐โ โ) = (๐โ โ)) |
6 | 5 | fveqeq2d 6896 |
. . . 4
โข (๐ = ๐ โ
((normโโ(๐โ โ)) = 1 โ
(normโโ(๐โ โ)) = 1)) |
7 | | fveq1 6887 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐โ๐ฅ) = (๐โ๐ฅ)) |
8 | | fveq1 6887 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐โ๐ฆ) = (๐โ๐ฆ)) |
9 | 7, 8 | oveq12d 7423 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih (๐โ๐ฆ))) |
10 | 9 | eqeq1d 2734 |
. . . . . . 7
โข (๐ = ๐ โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0)) |
11 | | fveq1 6887 |
. . . . . . . 8
โข (๐ = ๐ โ (๐โ(๐ฅ โจโ ๐ฆ)) = (๐โ(๐ฅ โจโ ๐ฆ))) |
12 | 7, 8 | oveq12d 7423 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐โ๐ฅ) +โ (๐โ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))) |
13 | 11, 12 | eqeq12d 2748 |
. . . . . . 7
โข (๐ = ๐ โ ((๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)) โ (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) |
14 | 10, 13 | anbi12d 631 |
. . . . . 6
โข (๐ = ๐ โ ((((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))) |
15 | 14 | imbi2d 340 |
. . . . 5
โข (๐ = ๐ โ ((๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) โ (๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))) |
16 | 15 | 2ralbidv 3218 |
. . . 4
โข (๐ = ๐ โ (โ๐ฅ โ Cโ
โ๐ฆ โ
Cโ (๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) โ โ๐ฅ โ Cโ
โ๐ฆ โ
Cโ (๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))) |
17 | 6, 16 | anbi12d 631 |
. . 3
โข (๐ = ๐ โ
(((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))) โ
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))))) |
18 | | df-hst 31452 |
. . 3
โข CHStates
= {๐ โ ( โ
โm Cโ ) โฃ
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))} |
19 | 17, 18 | elrab2 3685 |
. 2
โข (๐ โ CHStates โ (๐ โ ( โ
โm Cโ ) โง
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))))) |
20 | | 3anass 1095 |
. 2
โข ((๐:
Cโ โถ โ โง
(normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))) โ (๐: Cโ โถ
โ โง ((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))))) |
21 | 4, 19, 20 | 3bitr4i 302 |
1
โข (๐ โ CHStates โ (๐:
Cโ โถ โ โง
(normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))) |