0hmop

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

		Ref	Expression
	Assertion	0hmop	$⊢ 0_{hop} \in HrmOp$

Step	Hyp	Ref	Expression
1		ho0f	$⊢ 0_{hop} : ℋ ⟶ ℋ$
2		ho0val	$⊢ y \in ℋ \to 0_{hop} (y) = 0_{ℎ}$
3	2	oveq2d	$⊢ y \in ℋ \to x \cdot_{ih} 0_{hop} (y) = x \cdot_{ih} 0_{ℎ}$
4		hi02	$⊢ x \in ℋ \to x \cdot_{ih} 0_{ℎ} = 0$
5	3 4	sylan9eqr	$⊢ (x \in ℋ \land y \in ℋ) \to x \cdot_{ih} 0_{hop} (y) = 0$
6		ho0val	$⊢ x \in ℋ \to 0_{hop} (x) = 0_{ℎ}$
7	6	oveq1d	$⊢ x \in ℋ \to 0_{hop} (x) \cdot_{ih} y = 0_{ℎ} \cdot_{ih} y$
8		hi01	$⊢ y \in ℋ \to 0_{ℎ} \cdot_{ih} y = 0$
9	7 8	sylan9eq	$⊢ (x \in ℋ \land y \in ℋ) \to 0_{hop} (x) \cdot_{ih} y = 0$
10	5 9	eqtr4d	$⊢ (x \in ℋ \land y \in ℋ) \to x \cdot_{ih} 0_{hop} (y) = 0_{hop} (x) \cdot_{ih} y$
11	10	rgen2	$⊢ \forall x \in ℋ \forall y \in ℋ x \cdot_{ih} 0_{hop} (y) = 0_{hop} (x) \cdot_{ih} y$
12		elhmop	$⊢ 0_{hop} \in HrmOp \leftrightarrow (0_{hop} : ℋ ⟶ ℋ \land \forall x \in ℋ \forall y \in ℋ x \cdot_{ih} 0_{hop} (y) = 0_{hop} (x) \cdot_{ih} y)$
13	1 11 12	mpbir2an	$⊢ 0_{hop} \in HrmOp$

Metamath Proof Explorer