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

Metamath Proof Explorer

Theorem funadj

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

		Ref	Expression
	Assertion	funadj	⊢ Fun adj_ℎ

Proof

Step	Hyp	Ref	Expression
1		funopab	⊢ ( Fun { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) ) } ↔ ∀ 𝑡 ∃* 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) ) )
2		adjmo	⊢ ∃* 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) )
3		3simpc	⊢ ( ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) ) → ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) ) )
4	3	moimi	⊢ ( ∃* 𝑢 ( 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) ) → ∃* 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) ) )
5	2 4	ax-mp	⊢ ∃* 𝑢 ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) )
6	1 5	mpgbir	⊢ Fun { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) ) }
7		dfadj2	⊢ adj_ℎ = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) ) }
8	7	funeqi	⊢ ( Fun adj_ℎ ↔ Fun { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( 𝑡 : ℋ ⟶ ℋ ∧ 𝑢 : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( 𝑥 ·_ih ( 𝑡 ‘ 𝑦 ) ) = ( ( 𝑢 ‘ 𝑥 ) ·_ih 𝑦 ) ) } )
9	6 8	mpbir	⊢ Fun adj_ℎ