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 ) ) )