Theorem adjval2

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

	Ref	Expression
Assertion	adjval2	⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) = ( ℩ 𝑢 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		adjval	⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) = ( ℩ 𝑢 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) )
2		dmadjop	⊢ ( 𝑇 ∈ dom adjℎ → 𝑇 : ℋ ⟶ ℋ )
3		elmapi	⊢ ( 𝑢 ∈ ( ℋ ↑m ℋ ) → 𝑢 : ℋ ⟶ ℋ )
4		adjsym	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ) )
5		eqcom	⊢ ( ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) )
6	5	2ralbii	⊢ ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) )
7	4 6	bitrdi	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) )
8	2 3 7	syl2an	⊢ ( ( 𝑇 ∈ dom adjℎ ∧ 𝑢 ∈ ( ℋ ↑m ℋ ) ) → ( ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ↔ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) )
9	8	riotabidva	⊢ ( 𝑇 ∈ dom adjℎ → ( ℩ 𝑢 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·ih ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·ih 𝑦 ) ) = ( ℩ 𝑢 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) )
10	1 9	eqtrd	⊢ ( 𝑇 ∈ dom adjℎ → ( adjℎ ‘ 𝑇 ) = ( ℩ 𝑢 ∈ ( ℋ ↑m ℋ ) ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 𝑢 ‘ 𝑦 ) ) ) )