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

 Description: The adjoint of an operator belongs to the adjoint function's domain. (Note: the converse is dependent on our definition of function value, since it uses ndmfv 6682.) (Contributed by NM, 19-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression

Proof of Theorem dmadjrnb
StepHypRef Expression
1 dmadjrn 29676 . 2 (𝑇 ∈ dom adj → (adj𝑇) ∈ dom adj)
2 ax-hv0cl 28784 . . . . . . . . 9 0 ∈ ℋ
32n0ii 4274 . . . . . . . 8 ¬ ℋ = ∅
4 eqcom 2829 . . . . . . . 8 (∅ = ℋ ↔ ℋ = ∅)
53, 4mtbir 326 . . . . . . 7 ¬ ∅ = ℋ
6 dm0 5767 . . . . . . . 8 dom ∅ = ∅
76eqeq1i 2827 . . . . . . 7 (dom ∅ = ℋ ↔ ∅ = ℋ)
85, 7mtbir 326 . . . . . 6 ¬ dom ∅ = ℋ
9 fdm 6502 . . . . . 6 (∅: ℋ⟶ ℋ → dom ∅ = ℋ)
108, 9mto 200 . . . . 5 ¬ ∅: ℋ⟶ ℋ
11 dmadjop 29669 . . . . 5 (∅ ∈ dom adj → ∅: ℋ⟶ ℋ)
1210, 11mto 200 . . . 4 ¬ ∅ ∈ dom adj
13 ndmfv 6682 . . . . 5 𝑇 ∈ dom adj → (adj𝑇) = ∅)
1413eleq1d 2898 . . . 4 𝑇 ∈ dom adj → ((adj𝑇) ∈ dom adj ↔ ∅ ∈ dom adj))
1512, 14mtbiri 330 . . 3 𝑇 ∈ dom adj → ¬ (adj𝑇) ∈ dom adj)
1615con4i 114 . 2 ((adj𝑇) ∈ dom adj𝑇 ∈ dom adj)
171, 16impbii 212 1 (𝑇 ∈ dom adj ↔ (adj𝑇) ∈ dom adj)