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

Metamath Proof Explorer

Theorem hilid

Description: The group identity element of Hilbert space vector addition is the zero vector. (Contributed by NM, 16-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion hilid ( GId ‘ +ℎ ) = 0ℎ

Proof

Step Hyp Ref Expression
1 hilablo ⊢ +ℎ ∈ AbelOp
2 ablogrpo ⊢ ( +ℎ ∈ AbelOp → +ℎ ∈ GrpOp )
3 1 2 ax-mp ⊢ +ℎ ∈ GrpOp
4 ax-hfvadd ⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
5 4 fdmi ⊢ dom +ℎ = ( ℋ × ℋ )
6 3 5 grporn ⊢ ℋ = ran +ℎ
7 eqid ⊢ ( GId ‘ +ℎ ) = ( GId ‘ +ℎ )
8 6 7 grpoidval ⊢ ( +ℎ ∈ GrpOp → ( GId ‘ +ℎ ) = ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 +ℎ 𝑥 ) = 𝑥 ) )
9 3 8 ax-mp ⊢ ( GId ‘ +ℎ ) = ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 +ℎ 𝑥 ) = 𝑥 )
10 hvaddlid ⊢ ( 𝑥 ∈ ℋ → ( 0ℎ +ℎ 𝑥 ) = 𝑥 )
11 10 rgen ⊢ ∀ 𝑥 ∈ ℋ ( 0ℎ +ℎ 𝑥 ) = 𝑥
12 ax-hv0cl ⊢ 0ℎ ∈ ℋ
13 6 grpoideu ⊢ ( +ℎ ∈ GrpOp → ∃! 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 +ℎ 𝑥 ) = 𝑥 )
14 3 13 ax-mp ⊢ ∃! 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 +ℎ 𝑥 ) = 𝑥
15 oveq1 ⊢ ( 𝑦 = 0ℎ → ( 𝑦 +ℎ 𝑥 ) = ( 0ℎ +ℎ 𝑥 ) )
16 15 eqeq1d ⊢ ( 𝑦 = 0ℎ → ( ( 𝑦 +ℎ 𝑥 ) = 𝑥 ↔ ( 0ℎ +ℎ 𝑥 ) = 𝑥 ) )
17 16 ralbidv ⊢ ( 𝑦 = 0ℎ → ( ∀ 𝑥 ∈ ℋ ( 𝑦 +ℎ 𝑥 ) = 𝑥 ↔ ∀ 𝑥 ∈ ℋ ( 0ℎ +ℎ 𝑥 ) = 𝑥 ) )
18 17 riota2 ⊢ ( ( 0ℎ ∈ ℋ ∧ ∃! 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 +ℎ 𝑥 ) = 𝑥 ) → ( ∀ 𝑥 ∈ ℋ ( 0ℎ +ℎ 𝑥 ) = 𝑥 ↔ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 +ℎ 𝑥 ) = 𝑥 ) = 0ℎ ) )
19 12 14 18 mp2an ⊢ ( ∀ 𝑥 ∈ ℋ ( 0ℎ +ℎ 𝑥 ) = 𝑥 ↔ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 +ℎ 𝑥 ) = 𝑥 ) = 0ℎ )
20 11 19 mpbi ⊢ ( ℩ 𝑦 ∈ ℋ ∀ 𝑥 ∈ ℋ ( 𝑦 +ℎ 𝑥 ) = 𝑥 ) = 0ℎ
21 9 20 eqtri ⊢ ( GId ‘ +ℎ ) = 0ℎ