Metamath Proof Explorer

Theorem ajfval

Description: The adjoint function. (Contributed by NM, 25-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ajfval.1 ⊢ X = BaseSet ⁡ U
ajfval.2 ⊢ Y = BaseSet ⁡ W
ajfval.3 ⊢ P = ⋅ 𝑖OLD ⁡ U
ajfval.4 ⊢ Q = ⋅ 𝑖OLD ⁡ W
ajfval.5 ⊢ A = U adj W
Assertion 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

Proof

Step Hyp Ref Expression
1 ajfval.1 ⊢ X = BaseSet ⁡ U
2 ajfval.2 ⊢ Y = BaseSet ⁡ W
3 ajfval.3 ⊢ P = ⋅ 𝑖OLD ⁡ U
4 ajfval.4 ⊢ Q = ⋅ 𝑖OLD ⁡ W
5 ajfval.5 ⊢ A = U adj W
6 fveq2 ⊢ u = U → BaseSet ⁡ u = BaseSet ⁡ U
7 6 1 eqtr4di ⊢ u = U → BaseSet ⁡ u = X
8 7 feq2d ⊢ u = U → t : BaseSet ⁡ u ⟶ BaseSet ⁡ w ↔ t : X ⟶ BaseSet ⁡ w
9 7 feq3d ⊢ u = U → s : BaseSet ⁡ w ⟶ BaseSet ⁡ u ↔ s : BaseSet ⁡ w ⟶ X
10 fveq2 ⊢ u = U → ⋅ 𝑖OLD ⁡ u = ⋅ 𝑖OLD ⁡ U
11 10 3 eqtr4di ⊢ u = U → ⋅ 𝑖OLD ⁡ u = P
12 11 oveqd ⊢ u = U → x ⋅ 𝑖OLD ⁡ u s ⁡ y = x P s ⁡ y
13 12 eqeq2d ⊢ u = U → t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y ↔ t ⁡ x ⋅ 𝑖OLD ⁡ w y = x P s ⁡ y
14 13 ralbidv ⊢ u = U → ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y ↔ ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x P s ⁡ y
15 7 14 raleqbidv ⊢ u = U → ∀ x ∈ BaseSet ⁡ u ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x ⋅ 𝑖OLD ⁡ u s ⁡ y ↔ ∀ x ∈ X ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x P s ⁡ y
16 8 9 15 3anbi123d ⊢ u = U → 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 : X ⟶ BaseSet ⁡ w ∧ s : BaseSet ⁡ w ⟶ X ∧ ∀ x ∈ X ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x P s ⁡ y
17 16 opabbidv ⊢ u = U → 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 : X ⟶ BaseSet ⁡ w ∧ s : BaseSet ⁡ w ⟶ X ∧ ∀ x ∈ X ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x P s ⁡ y
18 fveq2 ⊢ w = W → BaseSet ⁡ w = BaseSet ⁡ W
19 18 2 eqtr4di ⊢ w = W → BaseSet ⁡ w = Y
20 19 feq3d ⊢ w = W → t : X ⟶ BaseSet ⁡ w ↔ t : X ⟶ Y
21 19 feq2d ⊢ w = W → s : BaseSet ⁡ w ⟶ X ↔ s : Y ⟶ X
22 fveq2 ⊢ w = W → ⋅ 𝑖OLD ⁡ w = ⋅ 𝑖OLD ⁡ W
23 22 4 eqtr4di ⊢ w = W → ⋅ 𝑖OLD ⁡ w = Q
24 23 oveqd ⊢ w = W → t ⁡ x ⋅ 𝑖OLD ⁡ w y = t ⁡ x Q y
25 24 eqeq1d ⊢ w = W → t ⁡ x ⋅ 𝑖OLD ⁡ w y = x P s ⁡ y ↔ t ⁡ x Q y = x P s ⁡ y
26 19 25 raleqbidv ⊢ w = W → ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x P s ⁡ y ↔ ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y
27 26 ralbidv ⊢ w = W → ∀ x ∈ X ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x P s ⁡ y ↔ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y
28 20 21 27 3anbi123d ⊢ w = W → t : X ⟶ BaseSet ⁡ w ∧ s : BaseSet ⁡ w ⟶ X ∧ ∀ x ∈ X ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w y = x P s ⁡ y ↔ t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y
29 28 opabbidv ⊢ w = W → t s | t : X ⟶ BaseSet ⁡ w ∧ s : BaseSet ⁡ w ⟶ X ∧ ∀ x ∈ X ∀ y ∈ BaseSet ⁡ w t ⁡ x ⋅ 𝑖OLD ⁡ w 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
30 df-aj ⊢ adj = u ∈ NrmCVec , w ∈ NrmCVec ⟼ 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
31 ovex ⊢ Y X ∈ V
32 ovex ⊢ X Y ∈ V
33 31 32 xpex ⊢ Y X × X Y ∈ V
34 2 fvexi ⊢ Y ∈ V
35 1 fvexi ⊢ X ∈ V
36 34 35 elmap ⊢ t ∈ Y X ↔ t : X ⟶ Y
37 35 34 elmap ⊢ s ∈ X Y ↔ s : Y ⟶ X
38 36 37 anbi12i ⊢ t ∈ Y X ∧ s ∈ X Y ↔ t : X ⟶ Y ∧ s : Y ⟶ X
39 38 biimpri ⊢ t : X ⟶ Y ∧ s : Y ⟶ X → t ∈ Y X ∧ s ∈ X Y
40 39 3adant3 ⊢ t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y → t ∈ Y X ∧ s ∈ X Y
41 40 ssopab2i ⊢ t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ⊆ t s | t ∈ Y X ∧ s ∈ X Y
42 df-xp ⊢ Y X × X Y = t s | t ∈ Y X ∧ s ∈ X Y
43 41 42 sseqtrri ⊢ t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ⊆ Y X × X Y
44 33 43 ssexi ⊢ t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y ∈ V
45 17 29 30 44 ovmpo ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec → U adj W = t s | t : X ⟶ Y ∧ s : Y ⟶ X ∧ ∀ x ∈ X ∀ y ∈ Y t ⁡ x Q y = x P s ⁡ y
46 5 45 syl5eq ⊢ 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