Step |
Hyp |
Ref |
Expression |
1 |
|
hstrlem3a.1 |
|- S = ( x e. CH |-> ( ( projh ` x ) ` u ) ) |
2 |
|
pjhcl |
|- ( ( x e. CH /\ u e. ~H ) -> ( ( projh ` x ) ` u ) e. ~H ) |
3 |
2
|
ancoms |
|- ( ( u e. ~H /\ x e. CH ) -> ( ( projh ` x ) ` u ) e. ~H ) |
4 |
3
|
adantlr |
|- ( ( ( u e. ~H /\ ( normh ` u ) = 1 ) /\ x e. CH ) -> ( ( projh ` x ) ` u ) e. ~H ) |
5 |
4 1
|
fmptd |
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S : CH --> ~H ) |
6 |
|
helch |
|- ~H e. CH |
7 |
1
|
hstrlem2 |
|- ( ~H e. CH -> ( S ` ~H ) = ( ( projh ` ~H ) ` u ) ) |
8 |
6 7
|
ax-mp |
|- ( S ` ~H ) = ( ( projh ` ~H ) ` u ) |
9 |
8
|
fveq2i |
|- ( normh ` ( S ` ~H ) ) = ( normh ` ( ( projh ` ~H ) ` u ) ) |
10 |
|
pjch1 |
|- ( u e. ~H -> ( ( projh ` ~H ) ` u ) = u ) |
11 |
10
|
fveq2d |
|- ( u e. ~H -> ( normh ` ( ( projh ` ~H ) ` u ) ) = ( normh ` u ) ) |
12 |
|
id |
|- ( ( normh ` u ) = 1 -> ( normh ` u ) = 1 ) |
13 |
11 12
|
sylan9eq |
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( normh ` ( ( projh ` ~H ) ` u ) ) = 1 ) |
14 |
9 13
|
syl5eq |
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( normh ` ( S ` ~H ) ) = 1 ) |
15 |
1
|
hstrlem2 |
|- ( z e. CH -> ( S ` z ) = ( ( projh ` z ) ` u ) ) |
16 |
1
|
hstrlem2 |
|- ( w e. CH -> ( S ` w ) = ( ( projh ` w ) ` u ) ) |
17 |
15 16
|
oveqan12d |
|- ( ( z e. CH /\ w e. CH ) -> ( ( S ` z ) .ih ( S ` w ) ) = ( ( ( projh ` z ) ` u ) .ih ( ( projh ` w ) ` u ) ) ) |
18 |
17
|
3adant3 |
|- ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( ( S ` z ) .ih ( S ` w ) ) = ( ( ( projh ` z ) ` u ) .ih ( ( projh ` w ) ` u ) ) ) |
19 |
18
|
adantr |
|- ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( S ` z ) .ih ( S ` w ) ) = ( ( ( projh ` z ) ` u ) .ih ( ( projh ` w ) ` u ) ) ) |
20 |
|
pjoi0 |
|- ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( ( projh ` z ) ` u ) .ih ( ( projh ` w ) ` u ) ) = 0 ) |
21 |
19 20
|
eqtrd |
|- ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( S ` z ) .ih ( S ` w ) ) = 0 ) |
22 |
|
pjcjt2 |
|- ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( z C_ ( _|_ ` w ) -> ( ( projh ` ( z vH w ) ) ` u ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) ) |
23 |
22
|
imp |
|- ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( projh ` ( z vH w ) ) ` u ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) |
24 |
|
chjcl |
|- ( ( z e. CH /\ w e. CH ) -> ( z vH w ) e. CH ) |
25 |
1
|
hstrlem2 |
|- ( ( z vH w ) e. CH -> ( S ` ( z vH w ) ) = ( ( projh ` ( z vH w ) ) ` u ) ) |
26 |
24 25
|
syl |
|- ( ( z e. CH /\ w e. CH ) -> ( S ` ( z vH w ) ) = ( ( projh ` ( z vH w ) ) ` u ) ) |
27 |
26
|
3adant3 |
|- ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( S ` ( z vH w ) ) = ( ( projh ` ( z vH w ) ) ` u ) ) |
28 |
27
|
adantr |
|- ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( S ` ( z vH w ) ) = ( ( projh ` ( z vH w ) ) ` u ) ) |
29 |
15 16
|
oveqan12d |
|- ( ( z e. CH /\ w e. CH ) -> ( ( S ` z ) +h ( S ` w ) ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) |
30 |
29
|
3adant3 |
|- ( ( z e. CH /\ w e. CH /\ u e. ~H ) -> ( ( S ` z ) +h ( S ` w ) ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) |
31 |
30
|
adantr |
|- ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( S ` z ) +h ( S ` w ) ) = ( ( ( projh ` z ) ` u ) +h ( ( projh ` w ) ` u ) ) ) |
32 |
23 28 31
|
3eqtr4d |
|- ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) |
33 |
21 32
|
jca |
|- ( ( ( z e. CH /\ w e. CH /\ u e. ~H ) /\ z C_ ( _|_ ` w ) ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) |
34 |
33
|
3exp1 |
|- ( z e. CH -> ( w e. CH -> ( u e. ~H -> ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) ) ) |
35 |
34
|
com3r |
|- ( u e. ~H -> ( z e. CH -> ( w e. CH -> ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) ) ) |
36 |
35
|
adantr |
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( z e. CH -> ( w e. CH -> ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) ) ) |
37 |
36
|
ralrimdv |
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> ( z e. CH -> A. w e. CH ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) ) |
38 |
37
|
ralrimiv |
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> A. z e. CH A. w e. CH ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) |
39 |
|
ishst |
|- ( S e. CHStates <-> ( S : CH --> ~H /\ ( normh ` ( S ` ~H ) ) = 1 /\ A. z e. CH A. w e. CH ( z C_ ( _|_ ` w ) -> ( ( ( S ` z ) .ih ( S ` w ) ) = 0 /\ ( S ` ( z vH w ) ) = ( ( S ` z ) +h ( S ` w ) ) ) ) ) ) |
40 |
5 14 38 39
|
syl3anbrc |
|- ( ( u e. ~H /\ ( normh ` u ) = 1 ) -> S e. CHStates ) |