Metamath Proof Explorer

Theorem adjval2

Description: Value of the adjoint function. (Contributed by NM, 19-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion adjval2 ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T = ι u ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y

Proof

Step Hyp Ref Expression
1 adjval ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T = ι u ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y
2 dmadjop ⊢ T ∈ dom ⁡ adj h → T : ℋ ⟶ ℋ
3 elmapi ⊢ u ∈ ℋ ℋ → u : ℋ ⟶ ℋ
4 adjsym ⊢ T : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih u ⁡ y = T ⁡ x ⋅ ih y
5 eqcom ⊢ x ⋅ ih u ⁡ y = T ⁡ x ⋅ ih y ↔ T ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
6 5 2ralbii ⊢ ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih u ⁡ y = T ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
7 4 6 bitrdi ⊢ T : ℋ ⟶ ℋ ∧ u : ℋ ⟶ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
8 2 3 7 syl2an ⊢ T ∈ dom ⁡ adj h ∧ u ∈ ℋ ℋ → ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y ↔ ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
9 8 riotabidva ⊢ T ∈ dom ⁡ adj h → ι u ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℋ x ⋅ ih T ⁡ y = u ⁡ x ⋅ ih y = ι u ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y
10 1 9 eqtrd ⊢ T ∈ dom ⁡ adj h → adj h ⁡ T = ι u ∈ ℋ ℋ | ∀ x ∈ ℋ ∀ y ∈ ℋ T ⁡ x ⋅ ih y = x ⋅ ih u ⁡ y