Theorem shmulcl 31802

Description: Closure of vector scalar multiplication in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
shmulcl	⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ℎ 𝐵) ∈ 𝐻)

Proof of Theorem shmulcl

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		issh2 31793	. . . . 5 ⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))
2	1	simprbi 503	. . . 4 ⊢ (𝐻 ∈ Sℋ → (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻))
3	2	simprd 501	. . 3 ⊢ (𝐻 ∈ Sℋ → ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)
4		oveq1 7419	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ·ℎ 𝑦) = (𝐴 ·ℎ 𝑦))
5	4	eleq1d 2846	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ·ℎ 𝑦) ∈ 𝐻 ↔ (𝐴 ·ℎ 𝑦) ∈ 𝐻))
6		oveq2 7420	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ·ℎ 𝑦) = (𝐴 ·ℎ 𝐵))
7	6	eleq1d 2846	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ·ℎ 𝑦) ∈ 𝐻 ↔ (𝐴 ·ℎ 𝐵) ∈ 𝐻))
8	5, 7	rspc2v 3587	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝐻) → (∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻 → (𝐴 ·ℎ 𝐵) ∈ 𝐻))
9	3, 8	syl5com 32	. 2 ⊢ (𝐻 ∈ Sℋ → ((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ℎ 𝐵) ∈ 𝐻))
10	9	3impib 1134	1 ⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ℎ 𝐵) ∈ 𝐻)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077   ⊆ wss 3899  (class class class)co 7412  ℂcc 11179   ℋchba 31503   +_ℎ cva 31504   ·_ℎ csm 31505  0_ℎc0v 31508   S_ℋ csh 31512

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-hilex 31583  ax-hfvadd 31584  ax-hfvmul 31589

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7415  df-sh 31791

This theorem is used by:  shsubcl  31804  norm1exi  31834  hhssabloilem  31845  hhssnv  31848  shsel3  31899  shscli  31901  shintcli  31913  pjhthlem1  31975  h1de2bi  32138  h1de2ctlem  32139  spansni  32141  spansnmul  32148  spansnss  32155  spanunsni  32163  h1datomi  32165  pjmulii  32261  mayete3i  32312  imaelshi  32642  strlem1  32834  cdj1i  33017  cdj3lem1  33018