Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  pjadji Structured version   Visualization version   GIF version

 Description: A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.)
Hypothesis
Ref Expression
Assertion
Ref Expression
pjadji ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (((proj𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((proj𝐻)‘𝐵)))

StepHypRef Expression
1 fveq2 6437 . . . 4 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → ((proj𝐻)‘𝐴) = ((proj𝐻)‘if(𝐴 ∈ ℋ, 𝐴, 0)))
21oveq1d 6925 . . 3 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → (((proj𝐻)‘𝐴) ·ih 𝐵) = (((proj𝐻)‘if(𝐴 ∈ ℋ, 𝐴, 0)) ·ih 𝐵))
3 oveq1 6917 . . 3 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → (𝐴 ·ih ((proj𝐻)‘𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih ((proj𝐻)‘𝐵)))
42, 3eqeq12d 2840 . 2 (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0) → ((((proj𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((proj𝐻)‘𝐵)) ↔ (((proj𝐻)‘if(𝐴 ∈ ℋ, 𝐴, 0)) ·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih ((proj𝐻)‘𝐵))))
5 oveq2 6918 . . 3 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → (((proj𝐻)‘if(𝐴 ∈ ℋ, 𝐴, 0)) ·ih 𝐵) = (((proj𝐻)‘if(𝐴 ∈ ℋ, 𝐴, 0)) ·ih if(𝐵 ∈ ℋ, 𝐵, 0)))
6 fveq2 6437 . . . 4 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → ((proj𝐻)‘𝐵) = ((proj𝐻)‘if(𝐵 ∈ ℋ, 𝐵, 0)))
76oveq2d 6926 . . 3 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih ((proj𝐻)‘𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih ((proj𝐻)‘if(𝐵 ∈ ℋ, 𝐵, 0))))
85, 7eqeq12d 2840 . 2 (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0) → ((((proj𝐻)‘if(𝐴 ∈ ℋ, 𝐴, 0)) ·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih ((proj𝐻)‘𝐵)) ↔ (((proj𝐻)‘if(𝐴 ∈ ℋ, 𝐴, 0)) ·ih if(𝐵 ∈ ℋ, 𝐵, 0)) = (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih ((proj𝐻)‘if(𝐵 ∈ ℋ, 𝐵, 0)))))
9 pjadjt.1 . . 3 𝐻C
10 ifhvhv0 28430 . . 3 if(𝐴 ∈ ℋ, 𝐴, 0) ∈ ℋ
11 ifhvhv0 28430 . . 3 if(𝐵 ∈ ℋ, 𝐵, 0) ∈ ℋ
129, 10, 11pjadjii 29084 . 2 (((proj𝐻)‘if(𝐴 ∈ ℋ, 𝐴, 0)) ·ih if(𝐵 ∈ ℋ, 𝐵, 0)) = (if(𝐴 ∈ ℋ, 𝐴, 0) ·ih ((proj𝐻)‘if(𝐵 ∈ ℋ, 𝐵, 0)))
134, 8, 12dedth2h 4365 1 ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (((proj𝐻)‘𝐴) ·ih 𝐵) = (𝐴 ·ih ((proj𝐻)‘𝐵)))