Metamath Proof Explorer

Theorem ajval

Description: Value of the adjoint function. (Contributed by NM, 25-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ajval.1 ⊢ X = BaseSet ⁡ U
ajval.2 ⊢ Y = BaseSet ⁡ W
ajval.3 ⊢ P = ⋅ 𝑖OLD ⁡ U
ajval.4 ⊢ Q = ⋅ 𝑖OLD ⁡ W
ajval.5 ⊢ A = U adj W
Assertion ajval ⊢ U ∈ CPreHil OLD ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → A ⁡ T = ι s | s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y

Proof

Step Hyp Ref Expression
1 ajval.1 ⊢ X = BaseSet ⁡ U
2 ajval.2 ⊢ Y = BaseSet ⁡ W
3 ajval.3 ⊢ P = ⋅ 𝑖OLD ⁡ U
4 ajval.4 ⊢ Q = ⋅ 𝑖OLD ⁡ W
5 ajval.5 ⊢ A = U adj W
6 phnv ⊢ U ∈ CPreHil OLD → U ∈ NrmCVec
7 1 2 3 4 5 ajfval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → A = t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y
8 6 7 sylan ⊢ U ∈ CPreHil OLD ∧ W ∈ NrmCVec → A = t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y
9 8 fveq1d ⊢ U ∈ CPreHil OLD ∧ W ∈ NrmCVec → A ⁡ T = t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ⁡ T
10 9 3adant3 ⊢ U ∈ CPreHil OLD ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → A ⁡ T = t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ⁡ T
11 1 fvexi ⊢ X ∈ V
12 fex ⊢ T : X ⟶ Y ∧ X ∈ V → T ∈ V
13 11 12 mpan2 ⊢ T : X ⟶ Y → T ∈ V
14 eqid ⊢ t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y = t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y
15 feq1 ⊢ t = T → t : X ⟶ Y ↔ T : X ⟶ Y
16 fveq1 ⊢ t = T → t ⁡ x = T ⁡ x
17 16 oveq1d ⊢ t = T → t ⁡ x Q y = T ⁡ x Q y
18 17 eqeq1d ⊢ t = T → t ⁡ x Q y = x P s ⁡ y ↔ T ⁡ x Q y = x P s ⁡ y
19 18 2ralbidv ⊢ t = T → ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ↔ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y
20 15 19 3anbi13d ⊢ t = T → t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ↔ T : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y
21 14 20 fvopab5 ⊢ T ∈ V → t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ⁡ T = ι s | T : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y
22 13 21 syl ⊢ T : X ⟶ Y → t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ⁡ T = ι s | T : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y
23 3anass ⊢ T : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y ↔ T : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y
24 23 baib ⊢ T : X ⟶ Y → T : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y ↔ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y
25 24 iotabidv ⊢ T : X ⟶ Y → ι s | T : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y = ι s | s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y
26 22 25 eqtrd ⊢ T : X ⟶ Y → t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ⁡ T = ι s | s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y
27 26 3ad2ant3 ⊢ U ∈ CPreHil OLD ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ⁡ T = ι s | s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y
28 10 27 eqtrd ⊢ U ∈ CPreHil OLD ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → A ⁡ T = ι s | s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y T ⁡ x Q y = x P s ⁡ y