hhsssh - Hilbert Space Explorer

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

Theorem hhsssh 31602

Description: The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
hhsst.1	⊢ 𝑈 = ⟨⟨ +_ℎ , ·_ℎ ⟩, norm_ℎ⟩
hhsst.2	⊢ 𝑊 = ⟨⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩, (norm_ℎ ↾ 𝐻)⟩

**Assertion**
Ref	Expression
hhsssh	⊢ (𝐻 ∈ S_ℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ))

**Proof of Theorem hhsssh**
Step	Hyp	Ref	Expression
1		hhsst.1	. . . 4 ⊢ 𝑈 = ⟨⟨ +_ℎ , ·_ℎ ⟩, norm_ℎ⟩
2		hhsst.2	. . . 4 ⊢ 𝑊 = ⟨⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩, (norm_ℎ ↾ 𝐻)⟩
3	1, 2	hhsst 31599	. . 3 ⊢ (𝐻 ∈ S_ℋ → 𝑊 ∈ (SubSp‘𝑈))
4		shss 31543	. . 3 ⊢ (𝐻 ∈ S_ℋ → 𝐻 ⊆ ℋ)
5	3, 4	jca 520	. 2 ⊢ (𝐻 ∈ S_ℋ → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ))
6		eleq1 2851	. . 3 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝐻 ∈ S_ℋ ↔ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ∈ S_ℋ ))
7		eqid 2763	. . . 4 ⊢ ⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩ = ⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩
8		xpeq1 5677	. . . . . . . . . . . . 13 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝐻 × 𝐻) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × 𝐻))
9		xpeq2 5684	. . . . . . . . . . . . 13 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × 𝐻) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))
10	8, 9	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝐻 × 𝐻) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))
11	10	reseq2d 5980	. . . . . . . . . . 11 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( +_ℎ ↾ (𝐻 × 𝐻)) = ( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))))
12		xpeq2 5684	. . . . . . . . . . . 12 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (ℂ × 𝐻) = (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))
13	12	reseq2d 5980	. . . . . . . . . . 11 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( ·_ℎ ↾ (ℂ × 𝐻)) = ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))))
14	11, 13	opeq12d 4847	. . . . . . . . . 10 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩ = ⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩)
15		reseq2 5975	. . . . . . . . . 10 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (norm_ℎ ↾ 𝐻) = (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))
16	14, 15	opeq12d 4847	. . . . . . . . 9 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ⟨⟨( +_ℎ ↾ (𝐻 × 𝐻)), ( ·_ℎ ↾ (ℂ × 𝐻))⟩, (norm_ℎ ↾ 𝐻)⟩ = ⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩)
17	2, 16	eqtrid 2810	. . . . . . . 8 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → 𝑊 = ⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩)
18	17	eleq1d 2848	. . . . . . 7 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝑊 ∈ (SubSp‘𝑈) ↔ ⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩ ∈ (SubSp‘𝑈)))
19		sseq1 3963	. . . . . . 7 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (𝐻 ⊆ ℋ ↔ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆ ℋ))
20	18, 19	anbi12d 643	. . . . . 6 ⊢ (𝐻 = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ) ↔ (⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩ ∈ (SubSp‘𝑈) ∧ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆ ℋ)))
21		xpeq1 5677	. . . . . . . . . . . 12 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( ℋ × ℋ) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × ℋ))
22		xpeq2 5684	. . . . . . . . . . . 12 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × ℋ) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))
23	21, 22	eqtrd 2798	. . . . . . . . . . 11 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( ℋ × ℋ) = (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))
24	23	reseq2d 5980	. . . . . . . . . 10 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( +_ℎ ↾ ( ℋ × ℋ)) = ( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))))
25		xpeq2 5684	. . . . . . . . . . 11 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (ℂ × ℋ) = (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))
26	25	reseq2d 5980	. . . . . . . . . 10 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( ·_ℎ ↾ (ℂ × ℋ)) = ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))))
27	24, 26	opeq12d 4847	. . . . . . . . 9 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ⟨( +_ℎ ↾ ( ℋ × ℋ)), ( ·_ℎ ↾ (ℂ × ℋ))⟩ = ⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩)
28		reseq2 5975	. . . . . . . . 9 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (norm_ℎ ↾ ℋ) = (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))
29	27, 28	opeq12d 4847	. . . . . . . 8 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ⟨⟨( +_ℎ ↾ ( ℋ × ℋ)), ( ·_ℎ ↾ (ℂ × ℋ))⟩, (norm_ℎ ↾ ℋ)⟩ = ⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩)
30	29	eleq1d 2848	. . . . . . 7 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → (⟨⟨( +_ℎ ↾ ( ℋ × ℋ)), ( ·_ℎ ↾ (ℂ × ℋ))⟩, (norm_ℎ ↾ ℋ)⟩ ∈ (SubSp‘𝑈) ↔ ⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩ ∈ (SubSp‘𝑈)))
31		sseq1 3963	. . . . . . 7 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ( ℋ ⊆ ℋ ↔ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆ ℋ))
32	30, 31	anbi12d 643	. . . . . 6 ⊢ ( ℋ = if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) → ((⟨⟨( +_ℎ ↾ ( ℋ × ℋ)), ( ·_ℎ ↾ (ℂ × ℋ))⟩, (norm_ℎ ↾ ℋ)⟩ ∈ (SubSp‘𝑈) ∧ ℋ ⊆ ℋ) ↔ (⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩ ∈ (SubSp‘𝑈) ∧ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆ ℋ)))
33		ax-hfvadd 31333	. . . . . . . . . . . 12 ⊢ +_ℎ :( ℋ × ℋ)⟶ ℋ
34		ffn 6707	. . . . . . . . . . . 12 ⊢ ( +_ℎ :( ℋ × ℋ)⟶ ℋ → +_ℎ Fn ( ℋ × ℋ))
35		fnresdm 6656	. . . . . . . . . . . 12 ⊢ ( +_ℎ Fn ( ℋ × ℋ) → ( +_ℎ ↾ ( ℋ × ℋ)) = +_ℎ )
36	33, 34, 35	mp2b 10	. . . . . . . . . . 11 ⊢ ( +_ℎ ↾ ( ℋ × ℋ)) = +_ℎ
37		ax-hfvmul 31338	. . . . . . . . . . . 12 ⊢ ·_ℎ :(ℂ × ℋ)⟶ ℋ
38		ffn 6707	. . . . . . . . . . . 12 ⊢ ( ·_ℎ :(ℂ × ℋ)⟶ ℋ → ·_ℎ Fn (ℂ × ℋ))
39		fnresdm 6656	. . . . . . . . . . . 12 ⊢ ( ·_ℎ Fn (ℂ × ℋ) → ( ·_ℎ ↾ (ℂ × ℋ)) = ·_ℎ )
40	37, 38, 39	mp2b 10	. . . . . . . . . . 11 ⊢ ( ·_ℎ ↾ (ℂ × ℋ)) = ·_ℎ
41	36, 40	opeq12i 4844	. . . . . . . . . 10 ⊢ ⟨( +_ℎ ↾ ( ℋ × ℋ)), ( ·_ℎ ↾ (ℂ × ℋ))⟩ = ⟨ +_ℎ , ·_ℎ ⟩
42		normf 31456	. . . . . . . . . . 11 ⊢ norm_ℎ: ℋ⟶ℝ
43		ffn 6707	. . . . . . . . . . 11 ⊢ (norm_ℎ: ℋ⟶ℝ → norm_ℎ Fn ℋ)
44		fnresdm 6656	. . . . . . . . . . 11 ⊢ (norm_ℎ Fn ℋ → (norm_ℎ ↾ ℋ) = norm_ℎ)
45	42, 43, 44	mp2b 10	. . . . . . . . . 10 ⊢ (norm_ℎ ↾ ℋ) = norm_ℎ
46	41, 45	opeq12i 4844	. . . . . . . . 9 ⊢ ⟨⟨( +_ℎ ↾ ( ℋ × ℋ)), ( ·_ℎ ↾ (ℂ × ℋ))⟩, (norm_ℎ ↾ ℋ)⟩ = ⟨⟨ +_ℎ , ·_ℎ ⟩, norm_ℎ⟩
47	46, 1	eqtr4i 2789	. . . . . . . 8 ⊢ ⟨⟨( +_ℎ ↾ ( ℋ × ℋ)), ( ·_ℎ ↾ (ℂ × ℋ))⟩, (norm_ℎ ↾ ℋ)⟩ = 𝑈
48	1	hhnv 31498	. . . . . . . . 9 ⊢ 𝑈 ∈ NrmCVec
49		eqid 2763	. . . . . . . . . 10 ⊢ (SubSp‘𝑈) = (SubSp‘𝑈)
50	49	sspid 31058	. . . . . . . . 9 ⊢ (𝑈 ∈ NrmCVec → 𝑈 ∈ (SubSp‘𝑈))
51	48, 50	ax-mp 5	. . . . . . . 8 ⊢ 𝑈 ∈ (SubSp‘𝑈)
52	47, 51	eqeltri 2859	. . . . . . 7 ⊢ ⟨⟨( +_ℎ ↾ ( ℋ × ℋ)), ( ·_ℎ ↾ (ℂ × ℋ))⟩, (norm_ℎ ↾ ℋ)⟩ ∈ (SubSp‘𝑈)
53		ssid 3960	. . . . . . 7 ⊢ ℋ ⊆ ℋ
54	52, 53	pm3.2i 475	. . . . . 6 ⊢ (⟨⟨( +_ℎ ↾ ( ℋ × ℋ)), ( ·_ℎ ↾ (ℂ × ℋ))⟩, (norm_ℎ ↾ ℋ)⟩ ∈ (SubSp‘𝑈) ∧ ℋ ⊆ ℋ)
55	20, 32, 54	elimhyp 4554	. . . . 5 ⊢ (⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩ ∈ (SubSp‘𝑈) ∧ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆ ℋ)
56	55	simpli 488	. . . 4 ⊢ ⟨⟨( +_ℎ ↾ (if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))), ( ·_ℎ ↾ (ℂ × if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ)))⟩, (norm_ℎ ↾ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ))⟩ ∈ (SubSp‘𝑈)
57	55	simpri 490	. . . 4 ⊢ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ⊆ ℋ
58	1, 7, 56, 57	hhshsslem2 31601	. . 3 ⊢ if((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ), 𝐻, ℋ) ∈ S_ℋ
59	6, 58	dedth 4547	. 2 ⊢ ((𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ) → 𝐻 ∈ S_ℋ )
60	5, 59	impbii 212	1 ⊢ (𝐻 ∈ S_ℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 ⊆ wss 3906 ifcif 4488 ⟨cop 4596 × cxp 5661 ↾ cres 5665 Fn wfn 6533 ⟶wf 6534 ‘cfv 6538 ℂcc 11099 ℝcr 11100 NrmCVeccnv 30917 SubSpcss 31054 ℋchba 31252 +_ℎ cva 31253 ·_ℎ csm 31254 norm_ℎcno 31256 S_ℋ csh 31261

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178 ax-pre-sup 11179 ax-addf 11180 ax-mulf 11181 ax-hilex 31332 ax-hfvadd 31333 ax-hvcom 31334 ax-hvass 31335 ax-hv0cl 31336 ax-hvaddid 31337 ax-hfvmul 31338 ax-hvmulid 31339 ax-hvmulass 31340 ax-hvdistr1 31341 ax-hvdistr2 31342 ax-hvmul0 31343 ax-hfi 31412 ax-his1 31415 ax-his2 31416 ax-his3 31417 ax-his4 31418

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-1st 7987 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-map 8827 df-pm 8828 df-en 8945 df-dom 8946 df-sdom 8947 df-sup 9403 df-inf 9404 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-2 12304 df-3 12305 df-4 12306 df-n0 12506 df-z 12593 df-uz 12864 df-q 12974 df-rp 13018 df-xneg 13138 df-xadd 13139 df-xmul 13140 df-icc 13380 df-seq 14040 df-exp 14100 df-cj 15152 df-re 15153 df-im 15154 df-sqrt 15288 df-abs 15289 df-topgen 17497 df-psmet 21495 df-xmet 21496 df-met 21497 df-bl 21498 df-mopn 21499 df-top 23032 df-topon 23049 df-bases 23084 df-lm 23367 df-haus 23453 df-grpo 30826 df-gid 30827 df-ginv 30828 df-gdiv 30829 df-ablo 30878 df-vc 30892 df-nv 30925 df-va 30928 df-ba 30929 df-sm 30930 df-0v 30931 df-vs 30932 df-nmcv 30933 df-ims 30934 df-ssp 31055 df-hnorm 31301 df-hba 31302 df-hvsub 31304 df-hlim 31305 df-sh 31540 df-ch 31554 df-ch0 31586

This theorem is referenced by: hhsssh2 31603

W3C validator