Metamath Proof Explorer


Theorem jpi

Description: The function S , that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a Jauch-Piron state. Remark in Mayet p. 370. (See strlem3a for the proof that S is a state.) (Contributed by NM, 8-Apr-2001) (New usage is discouraged.)

Ref Expression
Hypotheses jp.1 S=xCnormprojxu2
jp.2 AC
jp.3 BC
Assertion jpi unormu=1SA=1SB=1SAB=1

Proof

Step Hyp Ref Expression
1 jp.1 S=xCnormprojxu2
2 jp.2 AC
3 jp.3 BC
4 elin uABuAuB
5 1 2 jplem2 unormu=1uASA=1
6 1 3 jplem2 unormu=1uBSB=1
7 5 6 anbi12d unormu=1uAuBSA=1SB=1
8 4 7 syl5bb unormu=1uABSA=1SB=1
9 2 3 chincli ABC
10 1 9 jplem2 unormu=1uABSAB=1
11 8 10 bitr3d unormu=1SA=1SB=1SAB=1