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

 Description: Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression

Proof of Theorem adj0
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ho0f 28919 . 2 0hop : ℋ⟶ ℋ
2 ho0val 28918 . . . . . 6 (𝑥 ∈ ℋ → ( 0hop𝑥) = 0)
32oveq1d 6828 . . . . 5 (𝑥 ∈ ℋ → (( 0hop𝑥) ·ih 𝑦) = (0 ·ih 𝑦))
4 hi01 28262 . . . . 5 (𝑦 ∈ ℋ → (0 ·ih 𝑦) = 0)
53, 4sylan9eq 2814 . . . 4 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (( 0hop𝑥) ·ih 𝑦) = 0)
6 ho0val 28918 . . . . . 6 (𝑦 ∈ ℋ → ( 0hop𝑦) = 0)
76oveq2d 6829 . . . . 5 (𝑦 ∈ ℋ → (𝑥 ·ih ( 0hop𝑦)) = (𝑥 ·ih 0))
8 hi02 28263 . . . . 5 (𝑥 ∈ ℋ → (𝑥 ·ih 0) = 0)
97, 8sylan9eqr 2816 . . . 4 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (𝑥 ·ih ( 0hop𝑦)) = 0)
105, 9eqtr4d 2797 . . 3 ((𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ) → (( 0hop𝑥) ·ih 𝑦) = (𝑥 ·ih ( 0hop𝑦)))
1110rgen2a 3115 . 2 𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (( 0hop𝑥) ·ih 𝑦) = (𝑥 ·ih ( 0hop𝑦))
12 adjeq 29103 . 2 (( 0hop : ℋ⟶ ℋ ∧ 0hop : ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (( 0hop𝑥) ·ih 𝑦) = (𝑥 ·ih ( 0hop𝑦))) → (adj‘ 0hop ) = 0hop )
131, 1, 11, 12mp3an 1573 1 (adj‘ 0hop ) = 0hop