This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) = ( ℩ 𝑤 ∈ ℋ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 adjcl ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℋ )
2 eqcom ⊢ ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih 𝑤 ) ↔ ( 𝑥 ·ih 𝑤 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) )
3 adj2 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑥 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) )
4 3 3com23 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) )
5 4 3expa ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) )
6 5 eqeq2d ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑥 ·ih 𝑤 ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) ↔ ( 𝑥 ·ih 𝑤 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) ) )
7 2 6 bitrid ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih 𝑤 ) ↔ ( 𝑥 ·ih 𝑤 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) ) )
8 7 ralbidva ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih 𝑤 ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih 𝑤 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) ) )
9 8 adantr ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih 𝑤 ) ↔ ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih 𝑤 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) ) )
10 simpr ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → 𝑤 ∈ ℋ )
11 1 adantr ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℋ )
12 hial2eq2 ⊢ ( ( 𝑤 ∈ ℋ ∧ ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih 𝑤 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) ↔ 𝑤 = ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) )
13 10 11 12 syl2anc ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( 𝑥 ·ih 𝑤 ) = ( 𝑥 ·ih ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) ↔ 𝑤 = ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) )
14 9 13 bitrd ⊢ ( ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) ∧ 𝑤 ∈ ℋ ) → ( ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih 𝑤 ) ↔ 𝑤 = ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) ) )
15 1 14 riota5 ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) → ( ℩ 𝑤 ∈ ℋ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih 𝑤 ) ) = ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) )
16 15 eqcomd ⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝐴 ∈ ℋ ) → ( ( adjℎ ‘ 𝑇 ) ‘ 𝐴 ) = ( ℩ 𝑤 ∈ ℋ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝐴 ) = ( 𝑥 ·ih 𝑤 ) ) )