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 𝑤 ) ) )