Step | Hyp | Ref
| Expression |
1 | | ax-hilex 29983 |
. . . 4
โข โ
โ V |
2 | | chex 30210 |
. . . 4
โข
Cโ โ V |
3 | 1, 2 | elmap 8816 |
. . 3
โข (๐ โ ( โ
โm Cโ ) โ ๐: Cโ โถ
โ) |
4 | 3 | anbi1i 625 |
. 2
โข ((๐ โ ( โ
โm Cโ ) โง
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))) โ (๐: Cโ โถ
โ โง ((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))))) |
5 | | fveq1 6846 |
. . . . 5
โข (๐ = ๐ โ (๐โ โ) = (๐โ โ)) |
6 | 5 | fveqeq2d 6855 |
. . . 4
โข (๐ = ๐ โ
((normโโ(๐โ โ)) = 1 โ
(normโโ(๐โ โ)) = 1)) |
7 | | fveq1 6846 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐โ๐ฅ) = (๐โ๐ฅ)) |
8 | | fveq1 6846 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐โ๐ฆ) = (๐โ๐ฆ)) |
9 | 7, 8 | oveq12d 7380 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = ((๐โ๐ฅ) ยทih (๐โ๐ฆ))) |
10 | 9 | eqeq1d 2739 |
. . . . . . 7
โข (๐ = ๐ โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โ ((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0)) |
11 | | fveq1 6846 |
. . . . . . . 8
โข (๐ = ๐ โ (๐โ(๐ฅ โจโ ๐ฆ)) = (๐โ(๐ฅ โจโ ๐ฆ))) |
12 | 7, 8 | oveq12d 7380 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐โ๐ฅ) +โ (๐โ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))) |
13 | 11, 12 | eqeq12d 2753 |
. . . . . . 7
โข (๐ = ๐ โ ((๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)) โ (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) |
14 | 10, 13 | anbi12d 632 |
. . . . . 6
โข (๐ = ๐ โ ((((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))) |
15 | 14 | imbi2d 341 |
. . . . 5
โข (๐ = ๐ โ ((๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) โ (๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))) |
16 | 15 | 2ralbidv 3213 |
. . . 4
โข (๐ = ๐ โ (โ๐ฅ โ Cโ
โ๐ฆ โ
Cโ (๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))) โ โ๐ฅ โ Cโ
โ๐ฆ โ
Cโ (๐ฅ โ (โฅโ๐ฆ) โ (((๐โ๐ฅ) ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))) |
17 | 6, 16 | anbi12d 632 |
. . 3
โข (๐ = ๐ โ
(((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))) โ
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))))) |
18 | | df-hst 31196 |
. . 3
โข CHStates
= {๐ โ ( โ
โm Cโ ) โฃ
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))} |
19 | 17, 18 | elrab2 3653 |
. 2
โข (๐ โ CHStates โ (๐ โ ( โ
โm Cโ ) โง
((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))))) |
20 | | 3anass 1096 |
. 2
โข ((๐:
Cโ โถ โ โง
(normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))) โ (๐: Cโ โถ
โ โง ((normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ))))))) |
21 | 4, 19, 20 | 3bitr4i 303 |
1
โข (๐ โ CHStates โ (๐:
Cโ โถ โ โง
(normโโ(๐โ โ)) = 1 โง โ๐ฅ โ
Cโ โ๐ฆ โ Cโ
(๐ฅ โ
(โฅโ๐ฆ) โ
(((๐โ๐ฅ)
ยทih (๐โ๐ฆ)) = 0 โง (๐โ(๐ฅ โจโ ๐ฆ)) = ((๐โ๐ฅ) +โ (๐โ๐ฆ)))))) |