Theorem issh2 31145

Description: Subspace 𝐻 of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. Definition of [Beran] p. 95. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.)

Assertion

Ref	Expression
issh2	⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))

Distinct variable group:   𝑥,𝑦,𝐻

Proof of Theorem issh2

Step	Hyp	Ref	Expression
1		issh 31144	. 2 ⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻)))
2		ax-hfvadd 30936	. . . . . . 7 ⊢ +ℎ :( ℋ × ℋ)⟶ ℋ
3		ffun 6694	. . . . . . 7 ⊢ ( +ℎ :( ℋ × ℋ)⟶ ℋ → Fun +ℎ )
4	2, 3	ax-mp 5	. . . . . 6 ⊢ Fun +ℎ
5		xpss12 5656	. . . . . . . 8 ⊢ ((𝐻 ⊆ ℋ ∧ 𝐻 ⊆ ℋ) → (𝐻 × 𝐻) ⊆ ( ℋ × ℋ))
6	5	anidms 566	. . . . . . 7 ⊢ (𝐻 ⊆ ℋ → (𝐻 × 𝐻) ⊆ ( ℋ × ℋ))
7	2	fdmi 6702	. . . . . . 7 ⊢ dom +ℎ = ( ℋ × ℋ)
8	6, 7	sseqtrrdi 3991	. . . . . 6 ⊢ (𝐻 ⊆ ℋ → (𝐻 × 𝐻) ⊆ dom +ℎ )
9		funimassov 7569	. . . . . 6 ⊢ ((Fun +ℎ ∧ (𝐻 × 𝐻) ⊆ dom +ℎ ) → (( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ↔ ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻))
10	4, 8, 9	sylancr 587	. . . . 5 ⊢ (𝐻 ⊆ ℋ → (( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ↔ ∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻))
11		ax-hfvmul 30941	. . . . . . 7 ⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ
12		ffun 6694	. . . . . . 7 ⊢ ( ·ℎ :(ℂ × ℋ)⟶ ℋ → Fun ·ℎ )
13	11, 12	ax-mp 5	. . . . . 6 ⊢ Fun ·ℎ
14		xpss2 5661	. . . . . . 7 ⊢ (𝐻 ⊆ ℋ → (ℂ × 𝐻) ⊆ (ℂ × ℋ))
15	11	fdmi 6702	. . . . . . 7 ⊢ dom ·ℎ = (ℂ × ℋ)
16	14, 15	sseqtrrdi 3991	. . . . . 6 ⊢ (𝐻 ⊆ ℋ → (ℂ × 𝐻) ⊆ dom ·ℎ )
17		funimassov 7569	. . . . . 6 ⊢ ((Fun ·ℎ ∧ (ℂ × 𝐻) ⊆ dom ·ℎ ) → (( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻 ↔ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻))
18	13, 16, 17	sylancr 587	. . . . 5 ⊢ (𝐻 ⊆ ℋ → (( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻 ↔ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻))
19	10, 18	anbi12d 632	. . . 4 ⊢ (𝐻 ⊆ ℋ → ((( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻) ↔ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))
20	19	adantr 480	. . 3 ⊢ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) → ((( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻) ↔ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))
21	20	pm5.32i 574	. 2 ⊢ (((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (( +ℎ “ (𝐻 × 𝐻)) ⊆ 𝐻 ∧ ( ·ℎ “ (ℂ × 𝐻)) ⊆ 𝐻)) ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))
22	1, 21	bitri 275	1 ⊢ (𝐻 ∈ Sℋ ↔ ((𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻) ∧ (∀𝑥 ∈ 𝐻 ∀𝑦 ∈ 𝐻 (𝑥 +ℎ 𝑦) ∈ 𝐻 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝐻 (𝑥 ·ℎ 𝑦) ∈ 𝐻)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∀wral 3045   ⊆ wss 3917   × cxp 5639  dom cdm 5641   “ cima 5644  Fun wfun 6508  ⟶wf 6510  (class class class)co 7390  ℂcc 11073   ℋchba 30855   +_ℎ cva 30856   ·_ℎ csm 30857  0_ℎc0v 30860   S_ℋ csh 30864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-hilex 30935  ax-hfvadd 30936  ax-hfvmul 30941

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-sh 31143

This theorem is referenced by:  shaddcl  31153  shmulcl  31154  issh3  31155  helch  31179  hsn0elch  31184  hhshsslem2  31204  ocsh  31219  shscli  31253  shintcli  31265  imaelshi  31994