idhmop

Description: The Hilbert space identity operator is a Hermitian operator. (Contributed by NM, 22-Apr-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	idhmop	$⊢ I_{op} \in HrmOp$

Step	Hyp	Ref	Expression
1		hoif	$⊢ I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ$
2		f1of	$⊢ I_{op} : ℋ \underset{1-1 onto}{⟶} ℋ \to I_{op} : ℋ ⟶ ℋ$
3	1 2	ax-mp	$⊢ I_{op} : ℋ ⟶ ℋ$
4		hoival	$⊢ x \in ℋ \to I_{op} (x) = x$
5	4	eqcomd	$⊢ x \in ℋ \to x = I_{op} (x)$
6		hoival	$⊢ y \in ℋ \to I_{op} (y) = y$
7	5 6	oveqan12d	$⊢ (x \in ℋ \land y \in ℋ) \to x \cdot_{ih} I_{op} (y) = I_{op} (x) \cdot_{ih} y$
8	7	rgen2	$⊢ \forall x \in ℋ \forall y \in ℋ x \cdot_{ih} I_{op} (y) = I_{op} (x) \cdot_{ih} y$
9		elhmop	$⊢ I_{op} \in HrmOp \leftrightarrow (I_{op} : ℋ ⟶ ℋ \land \forall x \in ℋ \forall y \in ℋ x \cdot_{ih} I_{op} (y) = I_{op} (x) \cdot_{ih} y)$
10	3 8 9	mpbir2an	$⊢ I_{op} \in HrmOp$

Metamath Proof Explorer