df0op2

Description: Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	df0op2	$⊢ 0_{hop} = ℋ \times 0_{ℋ}$

Step	Hyp	Ref	Expression
1		ho0f	$⊢ 0_{hop} : ℋ ⟶ ℋ$
2		ffn	$⊢ 0_{hop} : ℋ ⟶ ℋ \to 0_{hop} Fn ℋ$
3	1 2	ax-mp	$⊢ 0_{hop} Fn ℋ$
4		ho0val	$⊢ x \in ℋ \to 0_{hop} (x) = 0_{ℎ}$
5	4	rgen	$⊢ \forall x \in ℋ 0_{hop} (x) = 0_{ℎ}$
6		fconstfv	$⊢ 0_{hop} : ℋ ⟶ \{0_{ℎ}\} \leftrightarrow (0_{hop} Fn ℋ \land \forall x \in ℋ 0_{hop} (x) = 0_{ℎ})$
7	3 5 6	mpbir2an	$⊢ 0_{hop} : ℋ ⟶ \{0_{ℎ}\}$
8		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
9	8	elexi	$⊢ 0_{ℎ} \in V$
10	9	fconst2	$⊢ 0_{hop} : ℋ ⟶ \{0_{ℎ}\} \leftrightarrow 0_{hop} = ℋ \times \{0_{ℎ}\}$
11	7 10	mpbi	$⊢ 0_{hop} = ℋ \times \{0_{ℎ}\}$
12		df-ch0	$⊢ 0_{ℋ} = \{0_{ℎ}\}$
13	12	xpeq2i	$⊢ ℋ \times 0_{ℋ} = ℋ \times \{0_{ℎ}\}$
14	11 13	eqtr4i	$⊢ 0_{hop} = ℋ \times 0_{ℋ}$

Metamath Proof Explorer