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 ( ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โˆง ( ๐ต โˆˆ Cโ„‹ โˆง ๐ด โŠ† ( โŠฅ โ€˜ ๐ต ) ) ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ( ๐ด โˆจโ„‹ ๐ต ) ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ด ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ต ) ) โ†‘ 2 ) ) )

Proof

Step Hyp Ref Expression
1 hstosum โŠข ( ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โˆง ( ๐ต โˆˆ Cโ„‹ โˆง ๐ด โŠ† ( โŠฅ โ€˜ ๐ต ) ) ) โ†’ ( ๐‘† โ€˜ ( ๐ด โˆจโ„‹ ๐ต ) ) = ( ( ๐‘† โ€˜ ๐ด ) +โ„Ž ( ๐‘† โ€˜ ๐ต ) ) )
2 1 fveq2d โŠข ( ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โˆง ( ๐ต โˆˆ Cโ„‹ โˆง ๐ด โŠ† ( โŠฅ โ€˜ ๐ต ) ) ) โ†’ ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ( ๐ด โˆจโ„‹ ๐ต ) ) ) = ( normโ„Ž โ€˜ ( ( ๐‘† โ€˜ ๐ด ) +โ„Ž ( ๐‘† โ€˜ ๐ต ) ) ) )
3 2 oveq1d โŠข ( ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โˆง ( ๐ต โˆˆ Cโ„‹ โˆง ๐ด โŠ† ( โŠฅ โ€˜ ๐ต ) ) ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ( ๐ด โˆจโ„‹ ๐ต ) ) ) โ†‘ 2 ) = ( ( normโ„Ž โ€˜ ( ( ๐‘† โ€˜ ๐ด ) +โ„Ž ( ๐‘† โ€˜ ๐ต ) ) ) โ†‘ 2 ) )
4 hstcl โŠข ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โ†’ ( ๐‘† โ€˜ ๐ด ) โˆˆ โ„‹ )
5 4 adantr โŠข ( ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โˆง ( ๐ต โˆˆ Cโ„‹ โˆง ๐ด โŠ† ( โŠฅ โ€˜ ๐ต ) ) ) โ†’ ( ๐‘† โ€˜ ๐ด ) โˆˆ โ„‹ )
6 hstcl โŠข ( ( ๐‘† โˆˆ CHStates โˆง ๐ต โˆˆ Cโ„‹ ) โ†’ ( ๐‘† โ€˜ ๐ต ) โˆˆ โ„‹ )
7 6 ad2ant2r โŠข ( ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โˆง ( ๐ต โˆˆ Cโ„‹ โˆง ๐ด โŠ† ( โŠฅ โ€˜ ๐ต ) ) ) โ†’ ( ๐‘† โ€˜ ๐ต ) โˆˆ โ„‹ )
8 hstorth โŠข ( ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โˆง ( ๐ต โˆˆ Cโ„‹ โˆง ๐ด โŠ† ( โŠฅ โ€˜ ๐ต ) ) ) โ†’ ( ( ๐‘† โ€˜ ๐ด ) ยทih ( ๐‘† โ€˜ ๐ต ) ) = 0 )
9 normpyth โŠข ( ( ( ๐‘† โ€˜ ๐ด ) โˆˆ โ„‹ โˆง ( ๐‘† โ€˜ ๐ต ) โˆˆ โ„‹ ) โ†’ ( ( ( ๐‘† โ€˜ ๐ด ) ยทih ( ๐‘† โ€˜ ๐ต ) ) = 0 โ†’ ( ( normโ„Ž โ€˜ ( ( ๐‘† โ€˜ ๐ด ) +โ„Ž ( ๐‘† โ€˜ ๐ต ) ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ด ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ต ) ) โ†‘ 2 ) ) ) )
10 9 3impia โŠข ( ( ( ๐‘† โ€˜ ๐ด ) โˆˆ โ„‹ โˆง ( ๐‘† โ€˜ ๐ต ) โˆˆ โ„‹ โˆง ( ( ๐‘† โ€˜ ๐ด ) ยทih ( ๐‘† โ€˜ ๐ต ) ) = 0 ) โ†’ ( ( normโ„Ž โ€˜ ( ( ๐‘† โ€˜ ๐ด ) +โ„Ž ( ๐‘† โ€˜ ๐ต ) ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ด ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ต ) ) โ†‘ 2 ) ) )
11 5 7 8 10 syl3anc โŠข ( ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โˆง ( ๐ต โˆˆ Cโ„‹ โˆง ๐ด โŠ† ( โŠฅ โ€˜ ๐ต ) ) ) โ†’ ( ( normโ„Ž โ€˜ ( ( ๐‘† โ€˜ ๐ด ) +โ„Ž ( ๐‘† โ€˜ ๐ต ) ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ด ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ต ) ) โ†‘ 2 ) ) )
12 3 11 eqtrd โŠข ( ( ( ๐‘† โˆˆ CHStates โˆง ๐ด โˆˆ Cโ„‹ ) โˆง ( ๐ต โˆˆ Cโ„‹ โˆง ๐ด โŠ† ( โŠฅ โ€˜ ๐ต ) ) ) โ†’ ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ( ๐ด โˆจโ„‹ ๐ต ) ) ) โ†‘ 2 ) = ( ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ด ) ) โ†‘ 2 ) + ( ( normโ„Ž โ€˜ ( ๐‘† โ€˜ ๐ต ) ) โ†‘ 2 ) ) )