Theorem adj0

Description: Adjoint of the zero operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adj0	⊢ ( adjℎ ‘ 0hop ) = 0hop

Proof

Step	Hyp	Ref	Expression
1		ho0f	⊢ 0hop : ℋ ⟶ ℋ
2		ho0val	⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
3	2	oveq1d	⊢ ( 𝑥 ∈ ℋ → ( ( 0hop ‘ 𝑥 ) ·ih 𝑦 ) = ( 0ℎ ·ih 𝑦 ) )
4		hi01	⊢ ( 𝑦 ∈ ℋ → ( 0ℎ ·ih 𝑦 ) = 0 )
5	3 4	sylan9eq	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 0hop ‘ 𝑥 ) ·ih 𝑦 ) = 0 )
6		ho0val	⊢ ( 𝑦 ∈ ℋ → ( 0hop ‘ 𝑦 ) = 0ℎ )
7	6	oveq2d	⊢ ( 𝑦 ∈ ℋ → ( 𝑥 ·ih ( 0hop ‘ 𝑦 ) ) = ( 𝑥 ·ih 0ℎ ) )
8		hi02	⊢ ( 𝑥 ∈ ℋ → ( 𝑥 ·ih 0ℎ ) = 0 )
9	7 8	sylan9eqr	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ih ( 0hop ‘ 𝑦 ) ) = 0 )
10	5 9	eqtr4d	⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( ( 0hop ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 0hop ‘ 𝑦 ) ) )
11	10	rgen2	⊢ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 0hop ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 0hop ‘ 𝑦 ) )
12		adjeq	⊢ ( ( 0hop : ℋ ⟶ ℋ ∧ 0hop : ℋ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℋ ∀ 𝑦 ∈ ℋ ( ( 0hop ‘ 𝑥 ) ·ih 𝑦 ) = ( 𝑥 ·ih ( 0hop ‘ 𝑦 ) ) ) → ( adjℎ ‘ 0hop ) = 0hop )
13	1 1 11 12	mp3an	⊢ ( adjℎ ‘ 0hop ) = 0hop