Metamath Proof Explorer

Theorem adjvalval

Description: Value of the value of the adjoint function. (Contributed by NM, 22-Feb-2006) (Proof shortened by Mario Carneiro, 10-Sep-2015) (New usage is discouraged.)

Ref Expression
Assertion adjvalval ⊢T∈dom⁡adjh∧A∈ℋ→adjh⁡T⁡A=ιw∈ℋ|∀x∈ℋT⁡x⋅ihA=x⋅ihw

Proof

Step Hyp Ref Expression
1 adjcl ⊢T∈dom⁡adjh∧A∈ℋ→adjh⁡T⁡A∈ℋ
2 eqcom ⊢T⁡x⋅ihA=x⋅ihw↔x⋅ihw=T⁡x⋅ihA
3 adj2 ⊢T∈dom⁡adjh∧x∈ℋ∧A∈ℋ→T⁡x⋅ihA=x⋅ihadjh⁡T⁡A
4 3 3com23 ⊢T∈dom⁡adjh∧A∈ℋ∧x∈ℋ→T⁡x⋅ihA=x⋅ihadjh⁡T⁡A
5 4 3expa ⊢T∈dom⁡adjh∧A∈ℋ∧x∈ℋ→T⁡x⋅ihA=x⋅ihadjh⁡T⁡A
6 5 eqeq2d ⊢T∈dom⁡adjh∧A∈ℋ∧x∈ℋ→x⋅ihw=T⁡x⋅ihA↔x⋅ihw=x⋅ihadjh⁡T⁡A
7 2 6 bitrid ⊢T∈dom⁡adjh∧A∈ℋ∧x∈ℋ→T⁡x⋅ihA=x⋅ihw↔x⋅ihw=x⋅ihadjh⁡T⁡A
8 7 ralbidva ⊢T∈dom⁡adjh∧A∈ℋ→∀x∈ℋT⁡x⋅ihA=x⋅ihw↔∀x∈ℋx⋅ihw=x⋅ihadjh⁡T⁡A
9 8 adantr ⊢T∈dom⁡adjh∧A∈ℋ∧w∈ℋ→∀x∈ℋT⁡x⋅ihA=x⋅ihw↔∀x∈ℋx⋅ihw=x⋅ihadjh⁡T⁡A
10 simpr ⊢T∈dom⁡adjh∧A∈ℋ∧w∈ℋ→w∈ℋ
11 1 adantr ⊢T∈dom⁡adjh∧A∈ℋ∧w∈ℋ→adjh⁡T⁡A∈ℋ
12 hial2eq2 ⊢w∈ℋ∧adjh⁡T⁡A∈ℋ→∀x∈ℋx⋅ihw=x⋅ihadjh⁡T⁡A↔w=adjh⁡T⁡A
13 10 11 12 syl2anc ⊢T∈dom⁡adjh∧A∈ℋ∧w∈ℋ→∀x∈ℋx⋅ihw=x⋅ihadjh⁡T⁡A↔w=adjh⁡T⁡A
14 9 13 bitrd ⊢T∈dom⁡adjh∧A∈ℋ∧w∈ℋ→∀x∈ℋT⁡x⋅ihA=x⋅ihw↔w=adjh⁡T⁡A
15 1 14 riota5 ⊢T∈dom⁡adjh∧A∈ℋ→ιw∈ℋ|∀x∈ℋT⁡x⋅ihA=x⋅ihw=adjh⁡T⁡A
16 15 eqcomd ⊢T∈dom⁡adjh∧A∈ℋ→adjh⁡T⁡A=ιw∈ℋ|∀x∈ℋT⁡x⋅ihA=x⋅ihw