This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmadjrnb

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 .) (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion dmadjrnb ( 𝑇 ∈ dom adjℎ ↔ ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )

Proof

Step Hyp Ref Expression
1 dmadjrn ⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
2 ax-hv0cl ⊢ 0ℎ ∈ ℋ
3 2 n0ii ⊢ ¬ ℋ = ∅
4 eqcom ⊢ ( ∅ = ℋ ↔ ℋ = ∅ )
5 3 4 mtbir ⊢ ¬ ∅ = ℋ
6 dm0 ⊢ dom ∅ = ∅
7 6 eqeq1i ⊢ ( dom ∅ = ℋ ↔ ∅ = ℋ )
8 5 7 mtbir ⊢ ¬ dom ∅ = ℋ
9 fdm ⊢ ( ∅ : ℋ ⟶ ℋ → dom ∅ = ℋ )
10 8 9 mto ⊢ ¬ ∅ : ℋ ⟶ ℋ
11 dmadjop ⊢ ( ∅ ∈ dom adjℎ → ∅ : ℋ ⟶ ℋ )
12 10 11 mto ⊢ ¬ ∅ ∈ dom adjℎ
13 ndmfv ⊢ ( ¬ 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) = ∅ )
14 13 eleq1d ⊢ ( ¬ 𝑇 ∈ dom adjℎ → ( ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ ↔ ∅ ∈ dom adjℎ ) )
15 12 14 mtbiri ⊢ ( ¬ 𝑇 ∈ dom adjℎ → ¬ ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )
16 15 con4i ⊢ ( ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ → 𝑇 ∈ dom adjℎ )
17 1 16 impbii ⊢ ( 𝑇 ∈ dom adjℎ ↔ ( adjℎ ‘ 𝑇 ) ∈ dom adjℎ )