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

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	⊢ ( 𝑇 ∈ 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 ( 𝑢 ‘ 𝑦 ) ) ) )