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 ⁡ + ℎ = ι y ∈ ℋ | ∀ x ∈ ℋ y + ℎ x = x
9 3 8 ax-mp ⊢ GId ⁡ + ℎ = ι y ∈ ℋ | ∀ x ∈ ℋ y + ℎ x = x
10 hvaddid2 ⊢ x ∈ ℋ → 0 ℎ + ℎ x = x
11 10 rgen ⊢ ∀ x ∈ ℋ 0 ℎ + ℎ x = x
12 ax-hv0cl ⊢ 0 ℎ ∈ ℋ
13 6 grpoideu ⊢ + ℎ ∈ GrpOp → ∃! y ∈ ℋ ∀ x ∈ ℋ y + ℎ x = x
14 3 13 ax-mp ⊢ ∃! y ∈ ℋ ∀ x ∈ ℋ y + ℎ x = x
15 oveq1 ⊢ y = 0 ℎ → y + ℎ x = 0 ℎ + ℎ x
16 15 eqeq1d ⊢ y = 0 ℎ → y + ℎ x = x ↔ 0 ℎ + ℎ x = x
17 16 ralbidv ⊢ y = 0 ℎ → ∀ x ∈ ℋ y + ℎ x = x ↔ ∀ x ∈ ℋ 0 ℎ + ℎ x = x
18 17 riota2 ⊢ 0 ℎ ∈ ℋ ∧ ∃! y ∈ ℋ ∀ x ∈ ℋ y + ℎ x = x → ∀ x ∈ ℋ 0 ℎ + ℎ x = x ↔ ι y ∈ ℋ | ∀ x ∈ ℋ y + ℎ x = x = 0 ℎ
19 12 14 18 mp2an ⊢ ∀ x ∈ ℋ 0 ℎ + ℎ x = x ↔ ι y ∈ ℋ | ∀ x ∈ ℋ y + ℎ x = x = 0 ℎ
20 11 19 mpbi ⊢ ι y ∈ ℋ | ∀ x ∈ ℋ y + ℎ x = x = 0 ℎ
21 9 20 eqtri ⊢ GId ⁡ + ℎ = 0 ℎ