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 ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ ⊥ ⁡ B → norm ℎ ⁡ S ⁡ A ∨ ℋ B 2 = norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ B 2

Proof

Step Hyp Ref Expression
1 hstosum ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ ⊥ ⁡ B → S ⁡ A ∨ ℋ B = S ⁡ A + ℎ S ⁡ B
2 1 fveq2d ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ ⊥ ⁡ B → norm ℎ ⁡ S ⁡ A ∨ ℋ B = norm ℎ ⁡ S ⁡ A + ℎ S ⁡ B
3 2 oveq1d ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ ⊥ ⁡ B → norm ℎ ⁡ S ⁡ A ∨ ℋ B 2 = norm ℎ ⁡ S ⁡ A + ℎ S ⁡ B 2
4 hstcl ⊢ S ∈ CHStates ∧ A ∈ C ℋ → S ⁡ A ∈ ℋ
5 4 adantr ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ ⊥ ⁡ B → S ⁡ A ∈ ℋ
6 hstcl ⊢ S ∈ CHStates ∧ B ∈ C ℋ → S ⁡ B ∈ ℋ
7 6 ad2ant2r ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ ⊥ ⁡ B → S ⁡ B ∈ ℋ
8 hstorth ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ ⊥ ⁡ B → S ⁡ A ⋅ ih S ⁡ B = 0
9 normpyth ⊢ S ⁡ A ∈ ℋ ∧ S ⁡ B ∈ ℋ → S ⁡ A ⋅ ih S ⁡ B = 0 → norm ℎ ⁡ S ⁡ A + ℎ S ⁡ B 2 = norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ B 2
10 9 3impia ⊢ S ⁡ A ∈ ℋ ∧ S ⁡ B ∈ ℋ ∧ S ⁡ A ⋅ ih S ⁡ B = 0 → norm ℎ ⁡ S ⁡ A + ℎ S ⁡ B 2 = norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ B 2
11 5 7 8 10 syl3anc ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ ⊥ ⁡ B → norm ℎ ⁡ S ⁡ A + ℎ S ⁡ B 2 = norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ B 2
12 3 11 eqtrd ⊢ S ∈ CHStates ∧ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ ⊥ ⁡ B → norm ℎ ⁡ S ⁡ A ∨ ℋ B 2 = norm ℎ ⁡ S ⁡ A 2 + norm ℎ ⁡ S ⁡ B 2