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

Metamath Proof Explorer

Theorem shsubcl

Description: Closure of vector subtraction in a subspace of a Hilbert space. (Contributed by NM, 18-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion shsubcl ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 −ℎ 𝐵 ) ∈ 𝐻 )

Proof

Step Hyp Ref Expression
1 shss ⊢ ( 𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ )
2 1 sseld ⊢ ( 𝐻 ∈ Sℋ → ( 𝐴 ∈ 𝐻 → 𝐴 ∈ ℋ ) )
3 1 sseld ⊢ ( 𝐻 ∈ Sℋ → ( 𝐵 ∈ 𝐻 → 𝐵 ∈ ℋ ) )
4 2 3 anim12d ⊢ ( 𝐻 ∈ Sℋ → ( ( 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ) )
5 4 3impib ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) )
6 hvsubval ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
7 5 6 syl ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
8 neg1cn ⊢ - 1 ∈ ℂ
9 shmulcl ⊢ ( ( 𝐻 ∈ Sℋ ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝐻 ) → ( - 1 ·ℎ 𝐵 ) ∈ 𝐻 )
10 8 9 mp3an2 ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐵 ∈ 𝐻 ) → ( - 1 ·ℎ 𝐵 ) ∈ 𝐻 )
11 10 3adant2 ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( - 1 ·ℎ 𝐵 ) ∈ 𝐻 )
12 shaddcl ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ ( - 1 ·ℎ 𝐵 ) ∈ 𝐻 ) → ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ 𝐻 )
13 11 12 syld3an3 ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ 𝐻 )
14 7 13 eqeltrd ⊢ ( ( 𝐻 ∈ Sℋ ∧ 𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻 ) → ( 𝐴 −ℎ 𝐵 ) ∈ 𝐻 )