HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  hilid Structured version   Visualization version   GIF version

Theorem hilid 28621
Description: The group identity element of Hilbert space vector addition is the zero vector. (Contributed by NM, 16-Apr-2007.) (New usage is discouraged.)
Assertion
Ref Expression
hilid (GId‘ + ) = 0

Proof of Theorem hilid
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hilablo 28620 . . . 4 + ∈ AbelOp
2 ablogrpo 28007 . . . 4 ( + ∈ AbelOp → + ∈ GrpOp)
31, 2ax-mp 5 . . 3 + ∈ GrpOp
4 ax-hfvadd 28460 . . . . . 6 + :( ℋ × ℋ)⟶ ℋ
54fdmi 6395 . . . . 5 dom + = ( ℋ × ℋ)
63, 5grporn 27981 . . . 4 ℋ = ran +
7 eqid 2794 . . . 4 (GId‘ + ) = (GId‘ + )
86, 7grpoidval 27973 . . 3 ( + ∈ GrpOp → (GId‘ + ) = (𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦 + 𝑥) = 𝑥))
93, 8ax-mp 5 . 2 (GId‘ + ) = (𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦 + 𝑥) = 𝑥)
10 hvaddid2 28483 . . . 4 (𝑥 ∈ ℋ → (0 + 𝑥) = 𝑥)
1110rgen 3114 . . 3 𝑥 ∈ ℋ (0 + 𝑥) = 𝑥
12 ax-hv0cl 28463 . . . 4 0 ∈ ℋ
136grpoideu 27969 . . . . 5 ( + ∈ GrpOp → ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦 + 𝑥) = 𝑥)
143, 13ax-mp 5 . . . 4 ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦 + 𝑥) = 𝑥
15 oveq1 7026 . . . . . . 7 (𝑦 = 0 → (𝑦 + 𝑥) = (0 + 𝑥))
1615eqeq1d 2796 . . . . . 6 (𝑦 = 0 → ((𝑦 + 𝑥) = 𝑥 ↔ (0 + 𝑥) = 𝑥))
1716ralbidv 3163 . . . . 5 (𝑦 = 0 → (∀𝑥 ∈ ℋ (𝑦 + 𝑥) = 𝑥 ↔ ∀𝑥 ∈ ℋ (0 + 𝑥) = 𝑥))
1817riota2 7002 . . . 4 ((0 ∈ ℋ ∧ ∃!𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦 + 𝑥) = 𝑥) → (∀𝑥 ∈ ℋ (0 + 𝑥) = 𝑥 ↔ (𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦 + 𝑥) = 𝑥) = 0))
1912, 14, 18mp2an 688 . . 3 (∀𝑥 ∈ ℋ (0 + 𝑥) = 𝑥 ↔ (𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦 + 𝑥) = 𝑥) = 0)
2011, 19mpbi 231 . 2 (𝑦 ∈ ℋ ∀𝑥 ∈ ℋ (𝑦 + 𝑥) = 𝑥) = 0
219, 20eqtri 2818 1 (GId‘ + ) = 0
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1522  wcel 2080  wral 3104  ∃!wreu 3106   × cxp 5444  cfv 6228  crio 6979  (class class class)co 7019  GrpOpcgr 27949  GIdcgi 27950  AbelOpcablo 28004  chba 28379   + cva 28380  0c0v 28384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322  ax-resscn 10443  ax-1cn 10444  ax-icn 10445  ax-addcl 10446  ax-addrcl 10447  ax-mulcl 10448  ax-mulrcl 10449  ax-mulcom 10450  ax-addass 10451  ax-mulass 10452  ax-distr 10453  ax-i2m1 10454  ax-1ne0 10455  ax-1rid 10456  ax-rnegex 10457  ax-rrecex 10458  ax-cnre 10459  ax-pre-lttri 10460  ax-pre-lttrn 10461  ax-pre-ltadd 10462  ax-hilex 28459  ax-hfvadd 28460  ax-hvcom 28461  ax-hvass 28462  ax-hv0cl 28463  ax-hvaddid 28464  ax-hfvmul 28465  ax-hvmulid 28466  ax-hvdistr2 28469  ax-hvmul0 28470
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-nel 3090  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-op 4481  df-uni 4748  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-id 5351  df-po 5365  df-so 5366  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-riota 6980  df-ov 7022  df-oprab 7023  df-mpo 7024  df-er 8142  df-en 8361  df-dom 8362  df-sdom 8363  df-pnf 10526  df-mnf 10527  df-ltxr 10529  df-sub 10721  df-neg 10722  df-grpo 27953  df-gid 27954  df-ablo 28005  df-hvsub 28431
This theorem is referenced by:  hhnv  28625  hh0v  28628  hhssabloilem  28721
  Copyright terms: Public domain W3C validator