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⁡adjh→adjh⁡T=ιu∈ℋℋ|∀x∈ℋ∀y∈ℋT⁡x⋅ihy=x⋅ihu⁡y

Proof

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