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		hvaddid2	⊢ ( 𝑥 ∈ ℋ → ( 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ℎ