Metamath Proof Explorer


Theorem hstrlem3

Description: Lemma for strong set of CH states theorem: the function S , that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. This lemma restates the hypotheses in a more convenient form to work with. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hstrlem3.1 S = x C proj x u
hstrlem3.2 φ u A B norm u = 1
hstrlem3.3 A C
hstrlem3.4 B C
Assertion hstrlem3 φ S CHStates

Proof

Step Hyp Ref Expression
1 hstrlem3.1 S = x C proj x u
2 hstrlem3.2 φ u A B norm u = 1
3 hstrlem3.3 A C
4 hstrlem3.4 B C
5 eldifi u A B u A
6 3 cheli u A u
7 5 6 syl u A B u
8 1 hstrlem3a u norm u = 1 S CHStates
9 7 8 sylan u A B norm u = 1 S CHStates
10 2 9 sylbi φ S CHStates