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

Metamath Proof Explorer

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