Theorem df0op2

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

	Ref	Expression
Assertion	df0op2	⊢ 0hop = ( ℋ × 0ℋ )

Proof

Step	Hyp	Ref	Expression
1		ho0f	⊢ 0hop : ℋ ⟶ ℋ
2		ffn	⊢ ( 0hop : ℋ ⟶ ℋ → 0hop Fn ℋ )
3	1 2	ax-mp	⊢ 0hop Fn ℋ
4		ho0val	⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
5	4	rgen	⊢ ∀ 𝑥 ∈ ℋ ( 0hop ‘ 𝑥 ) = 0ℎ
6		fconstfv	⊢ ( 0hop : ℋ ⟶ { 0ℎ } ↔ ( 0hop Fn ℋ ∧ ∀ 𝑥 ∈ ℋ ( 0hop ‘ 𝑥 ) = 0ℎ ) )
7	3 5 6	mpbir2an	⊢ 0hop : ℋ ⟶ { 0ℎ }
8		ax-hv0cl	⊢ 0ℎ ∈ ℋ
9	8	elexi	⊢ 0ℎ ∈ V
10	9	fconst2	⊢ ( 0hop : ℋ ⟶ { 0ℎ } ↔ 0hop = ( ℋ × { 0ℎ } ) )
11	7 10	mpbi	⊢ 0hop = ( ℋ × { 0ℎ } )
12		df-ch0	⊢ 0ℋ = { 0ℎ }
13	12	xpeq2i	⊢ ( ℋ × 0ℋ ) = ( ℋ × { 0ℎ } )
14	11 13	eqtr4i	⊢ 0hop = ( ℋ × 0ℋ )