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 ⊢ T ∈ dom ⁡ adj h ↔ adj h ⁡ T ∈ dom ⁡ adj h

Proof

Step Hyp Ref Expression
1 dmadjrn ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T ∈ dom ⁡ adj h
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 h → ∅ : ℋ ⟶ ℋ
12 10 11 mto ⊢ ¬ ∅ ∈ dom ⁡ adj h
13 ndmfv ⊢ ¬ T ∈ dom ⁡ adj h → adj h ⁡ T = ∅
14 13 eleq1d ⊢ ¬ T ∈ dom ⁡ adj h → adj h ⁡ T ∈ dom ⁡ adj h ↔ ∅ ∈ dom ⁡ adj h
15 12 14 mtbiri ⊢ ¬ T ∈ dom ⁡ adj h → ¬ adj h ⁡ T ∈ dom ⁡ adj h
16 15 con4i ⊢ adj h ⁡ T ∈ dom ⁡ adj h → T ∈ dom ⁡ adj h
17 1 16 impbii ⊢ T ∈ dom ⁡ adj h ↔ adj h ⁡ T ∈ dom ⁡ adj h