Metamath Proof Explorer

Theorem ajfuni

Description: The adjoint function is a function. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ajfuni.5 ⊢ A = U adj W
ajfuni.u ⊢ U ∈ CPreHil OLD
ajfuni.w ⊢ W ∈ NrmCVec
Assertion ajfuni ⊢ Fun ⁡ A

Proof

Step Hyp Ref Expression
1 ajfuni.5 ⊢ A = U adj W
2 ajfuni.u ⊢ U ∈ CPreHil OLD
3 ajfuni.w ⊢ W ∈ NrmCVec
4 funopab ⊢ Fun ⁡ t s | t : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y ↔ ∀ t ∃* s t : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y
5 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
6 eqid ⊢ ⋅ 𝑖OLD ⁡ U = ⋅ 𝑖OLD ⁡ U
7 5 6 2 ajmoi ⊢ ∃* s s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y
8 3simpc ⊢ t : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y → s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y
9 8 moimi ⊢ ∃* s s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y → ∃* s t : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y
10 7 9 ax-mp ⊢ ∃* s t : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y
11 4 10 mpgbir ⊢ Fun ⁡ t s | t : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y
12 2 phnvi ⊢ U ∈ NrmCVec
13 eqid ⊢ BaseSet ⁡ W = BaseSet ⁡ W
14 eqid ⊢ ⋅ 𝑖OLD ⁡ W = ⋅ 𝑖OLD ⁡ W
15 5 13 6 14 1 ajfval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → A = t s | t : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y
16 12 3 15 mp2an ⊢ A = t s | t : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y
17 16 funeqi ⊢ Fun ⁡ A ↔ Fun ⁡ t s | t : BaseSet ⁡ U ⟶ BaseSet ⁡ W ∧ s : BaseSet ⁡ W ⟶ BaseSet ⁡ U ∧ ∀ x ∈ BaseSet ⁡ U ∀ y ∈ BaseSet ⁡ W t ⁡ x ⋅ 𝑖OLD ⁡ W y = x ⋅ 𝑖OLD ⁡ U s ⁡ y
18 11 17 mpbir ⊢ Fun ⁡ A