Theorem 0hmop

Description: The identically zero function is a Hermitian operator. (Contributed by NM, 8-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	0hmop	⊢ 0hop ∈ HrmOp

Proof

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