Step | Hyp | Ref
| Expression |
1 | | pjhcl 30385 |
. . . . 5
โข ((๐ฅ โ
Cโ โง ๐ข โ โ) โ
((projโโ๐ฅ)โ๐ข) โ โ) |
2 | 1 | ancoms 460 |
. . . 4
โข ((๐ข โ โ โง ๐ฅ โ
Cโ ) โ
((projโโ๐ฅ)โ๐ข) โ โ) |
3 | 2 | adantlr 714 |
. . 3
โข (((๐ข โ โ โง
(normโโ๐ข) = 1) โง ๐ฅ โ Cโ )
โ ((projโโ๐ฅ)โ๐ข) โ โ) |
4 | | hstrlem3a.1 |
. . 3
โข ๐ = (๐ฅ โ Cโ
โฆ ((projโโ๐ฅ)โ๐ข)) |
5 | 3, 4 | fmptd 7067 |
. 2
โข ((๐ข โ โ โง
(normโโ๐ข) = 1) โ ๐: Cโ โถ
โ) |
6 | | helch 30227 |
. . . . 5
โข โ
โ Cโ |
7 | 4 | hstrlem2 31243 |
. . . . 5
โข ( โ
โ Cโ โ (๐โ โ) =
((projโโ โ)โ๐ข)) |
8 | 6, 7 | ax-mp 5 |
. . . 4
โข (๐โ โ) =
((projโโ โ)โ๐ข) |
9 | 8 | fveq2i 6850 |
. . 3
โข
(normโโ(๐โ โ)) =
(normโโ((projโโ
โ)โ๐ข)) |
10 | | pjch1 30654 |
. . . . 5
โข (๐ข โ โ โ
((projโโ โ)โ๐ข) = ๐ข) |
11 | 10 | fveq2d 6851 |
. . . 4
โข (๐ข โ โ โ
(normโโ((projโโ
โ)โ๐ข)) =
(normโโ๐ข)) |
12 | | id 22 |
. . . 4
โข
((normโโ๐ข) = 1 โ
(normโโ๐ข) = 1) |
13 | 11, 12 | sylan9eq 2797 |
. . 3
โข ((๐ข โ โ โง
(normโโ๐ข) = 1) โ
(normโโ((projโโ
โ)โ๐ข)) =
1) |
14 | 9, 13 | eqtrid 2789 |
. 2
โข ((๐ข โ โ โง
(normโโ๐ข) = 1) โ
(normโโ(๐โ โ)) = 1) |
15 | 4 | hstrlem2 31243 |
. . . . . . . . . . . 12
โข (๐ง โ
Cโ โ (๐โ๐ง) = ((projโโ๐ง)โ๐ข)) |
16 | 4 | hstrlem2 31243 |
. . . . . . . . . . . 12
โข (๐ค โ
Cโ โ (๐โ๐ค) = ((projโโ๐ค)โ๐ข)) |
17 | 15, 16 | oveqan12d 7381 |
. . . . . . . . . . 11
โข ((๐ง โ
Cโ โง ๐ค โ Cโ )
โ ((๐โ๐ง)
ยทih (๐โ๐ค)) = (((projโโ๐ง)โ๐ข) ยทih
((projโโ๐ค)โ๐ข))) |
18 | 17 | 3adant3 1133 |
. . . . . . . . . 10
โข ((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โ ((๐โ๐ง)
ยทih (๐โ๐ค)) = (((projโโ๐ง)โ๐ข) ยทih
((projโโ๐ค)โ๐ข))) |
19 | 18 | adantr 482 |
. . . . . . . . 9
โข (((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โง ๐ง โ
(โฅโ๐ค)) โ
((๐โ๐ง)
ยทih (๐โ๐ค)) = (((projโโ๐ง)โ๐ข) ยทih
((projโโ๐ค)โ๐ข))) |
20 | | pjoi0 30701 |
. . . . . . . . 9
โข (((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โง ๐ง โ
(โฅโ๐ค)) โ
(((projโโ๐ง)โ๐ข) ยทih
((projโโ๐ค)โ๐ข)) = 0) |
21 | 19, 20 | eqtrd 2777 |
. . . . . . . 8
โข (((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โง ๐ง โ
(โฅโ๐ค)) โ
((๐โ๐ง)
ยทih (๐โ๐ค)) = 0) |
22 | | pjcjt2 30676 |
. . . . . . . . . 10
โข ((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โ (๐ง โ
(โฅโ๐ค) โ
((projโโ(๐ง โจโ ๐ค))โ๐ข) = (((projโโ๐ง)โ๐ข) +โ
((projโโ๐ค)โ๐ข)))) |
23 | 22 | imp 408 |
. . . . . . . . 9
โข (((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โง ๐ง โ
(โฅโ๐ค)) โ
((projโโ(๐ง โจโ ๐ค))โ๐ข) = (((projโโ๐ง)โ๐ข) +โ
((projโโ๐ค)โ๐ข))) |
24 | | chjcl 30341 |
. . . . . . . . . . . 12
โข ((๐ง โ
Cโ โง ๐ค โ Cโ )
โ (๐ง
โจโ ๐ค)
โ Cโ ) |
25 | 4 | hstrlem2 31243 |
. . . . . . . . . . . 12
โข ((๐ง โจโ ๐ค) โ
Cโ โ (๐โ(๐ง โจโ ๐ค)) = ((projโโ(๐ง โจโ ๐ค))โ๐ข)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
โข ((๐ง โ
Cโ โง ๐ค โ Cโ )
โ (๐โ(๐ง โจโ ๐ค)) =
((projโโ(๐ง โจโ ๐ค))โ๐ข)) |
27 | 26 | 3adant3 1133 |
. . . . . . . . . 10
โข ((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โ (๐โ(๐ง โจโ ๐ค)) =
((projโโ(๐ง โจโ ๐ค))โ๐ข)) |
28 | 27 | adantr 482 |
. . . . . . . . 9
โข (((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โง ๐ง โ
(โฅโ๐ค)) โ
(๐โ(๐ง โจโ ๐ค)) =
((projโโ(๐ง โจโ ๐ค))โ๐ข)) |
29 | 15, 16 | oveqan12d 7381 |
. . . . . . . . . . 11
โข ((๐ง โ
Cโ โง ๐ค โ Cโ )
โ ((๐โ๐ง) +โ (๐โ๐ค)) = (((projโโ๐ง)โ๐ข) +โ
((projโโ๐ค)โ๐ข))) |
30 | 29 | 3adant3 1133 |
. . . . . . . . . 10
โข ((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โ ((๐โ๐ง) +โ (๐โ๐ค)) = (((projโโ๐ง)โ๐ข) +โ
((projโโ๐ค)โ๐ข))) |
31 | 30 | adantr 482 |
. . . . . . . . 9
โข (((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โง ๐ง โ
(โฅโ๐ค)) โ
((๐โ๐ง) +โ (๐โ๐ค)) = (((projโโ๐ง)โ๐ข) +โ
((projโโ๐ค)โ๐ข))) |
32 | 23, 28, 31 | 3eqtr4d 2787 |
. . . . . . . 8
โข (((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โง ๐ง โ
(โฅโ๐ค)) โ
(๐โ(๐ง โจโ ๐ค)) = ((๐โ๐ง) +โ (๐โ๐ค))) |
33 | 21, 32 | jca 513 |
. . . . . . 7
โข (((๐ง โ
Cโ โง ๐ค โ Cโ
โง ๐ข โ โ)
โง ๐ง โ
(โฅโ๐ค)) โ
(((๐โ๐ง)
ยทih (๐โ๐ค)) = 0 โง (๐โ(๐ง โจโ ๐ค)) = ((๐โ๐ง) +โ (๐โ๐ค)))) |
34 | 33 | 3exp1 1353 |
. . . . . 6
โข (๐ง โ
Cโ โ (๐ค โ Cโ
โ (๐ข โ โ
โ (๐ง โ
(โฅโ๐ค) โ
(((๐โ๐ง)
ยทih (๐โ๐ค)) = 0 โง (๐โ(๐ง โจโ ๐ค)) = ((๐โ๐ง) +โ (๐โ๐ค))))))) |
35 | 34 | com3r 87 |
. . . . 5
โข (๐ข โ โ โ (๐ง โ
Cโ โ (๐ค โ Cโ
โ (๐ง โ
(โฅโ๐ค) โ
(((๐โ๐ง)
ยทih (๐โ๐ค)) = 0 โง (๐โ(๐ง โจโ ๐ค)) = ((๐โ๐ง) +โ (๐โ๐ค))))))) |
36 | 35 | adantr 482 |
. . . 4
โข ((๐ข โ โ โง
(normโโ๐ข) = 1) โ (๐ง โ Cโ
โ (๐ค โ
Cโ โ (๐ง โ (โฅโ๐ค) โ (((๐โ๐ง) ยทih (๐โ๐ค)) = 0 โง (๐โ(๐ง โจโ ๐ค)) = ((๐โ๐ง) +โ (๐โ๐ค))))))) |
37 | 36 | ralrimdv 3150 |
. . 3
โข ((๐ข โ โ โง
(normโโ๐ข) = 1) โ (๐ง โ Cโ
โ โ๐ค โ
Cโ (๐ง โ (โฅโ๐ค) โ (((๐โ๐ง) ยทih (๐โ๐ค)) = 0 โง (๐โ(๐ง โจโ ๐ค)) = ((๐โ๐ง) +โ (๐โ๐ค)))))) |
38 | 37 | ralrimiv 3143 |
. 2
โข ((๐ข โ โ โง
(normโโ๐ข) = 1) โ โ๐ง โ Cโ
โ๐ค โ
Cโ (๐ง โ (โฅโ๐ค) โ (((๐โ๐ง) ยทih (๐โ๐ค)) = 0 โง (๐โ(๐ง โจโ ๐ค)) = ((๐โ๐ง) +โ (๐โ๐ค))))) |
39 | | ishst 31198 |
. 2
โข (๐ โ CHStates โ (๐:
Cโ โถ โ โง
(normโโ(๐โ โ)) = 1 โง โ๐ง โ
Cโ โ๐ค โ Cโ
(๐ง โ
(โฅโ๐ค) โ
(((๐โ๐ง)
ยทih (๐โ๐ค)) = 0 โง (๐โ(๐ง โจโ ๐ค)) = ((๐โ๐ง) +โ (๐โ๐ค)))))) |
40 | 5, 14, 38, 39 | syl3anbrc 1344 |
1
โข ((๐ข โ โ โง
(normโโ๐ข) = 1) โ ๐ โ CHStates) |