Metamath Proof Explorer

Theorem hstpyth

Description: Pythagorean property of a Hilbert-space-valued state for orthogonal vectors A and B . (Contributed by NM, 26-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstpyth 
|- ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( ( normh ` ( S ` ( A vH B ) ) ) ^ 2 ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` B ) ) ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 hstosum 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( S ` ( A vH B ) ) = ( ( S ` A ) +h ( S ` B ) ) )
2 1 fveq2d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( normh ` ( S ` ( A vH B ) ) ) = ( normh ` ( ( S ` A ) +h ( S ` B ) ) ) )
3 2 oveq1d 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( ( normh ` ( S ` ( A vH B ) ) ) ^ 2 ) = ( ( normh ` ( ( S ` A ) +h ( S ` B ) ) ) ^ 2 ) )
4 hstcl 
 |-  ( ( S e. CHStates /\ A e. CH ) -> ( S ` A ) e. ~H )
5 4 adantr 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( S ` A ) e. ~H )
6 hstcl 
 |-  ( ( S e. CHStates /\ B e. CH ) -> ( S ` B ) e. ~H )
7 6 ad2ant2r 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( S ` B ) e. ~H )
8 hstorth 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( ( S ` A ) .ih ( S ` B ) ) = 0 )
9 normpyth 
 |-  ( ( ( S ` A ) e. ~H /\ ( S ` B ) e. ~H ) -> ( ( ( S ` A ) .ih ( S ` B ) ) = 0 -> ( ( normh ` ( ( S ` A ) +h ( S ` B ) ) ) ^ 2 ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` B ) ) ^ 2 ) ) ) )
10 9 3impia 
 |-  ( ( ( S ` A ) e. ~H /\ ( S ` B ) e. ~H /\ ( ( S ` A ) .ih ( S ` B ) ) = 0 ) -> ( ( normh ` ( ( S ` A ) +h ( S ` B ) ) ) ^ 2 ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` B ) ) ^ 2 ) ) )
11 5 7 8 10 syl3anc 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( ( normh ` ( ( S ` A ) +h ( S ` B ) ) ) ^ 2 ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` B ) ) ^ 2 ) ) )
12 3 11 eqtrd 
 |-  ( ( ( S e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ ( _|_ ` B ) ) ) -> ( ( normh ` ( S ` ( A vH B ) ) ) ^ 2 ) = ( ( ( normh ` ( S ` A ) ) ^ 2 ) + ( ( normh ` ( S ` B ) ) ^ 2 ) ) )