This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ℋ )