Metamath Proof Explorer

Theorem hhsssh

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

Ref Expression
Hypotheses hhsst.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
hhsst.2 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
Assertion hhsssh ( 𝐻 ∈ Sℋ ↔ ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) )

Proof

Step Hyp Ref Expression
1 hhsst.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 hhsst.2 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
3 1 2 hhsst ⊢ ( 𝐻 ∈ Sℋ → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
4 shss ⊢ ( 𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ )
5 3 4 jca ⊢ ( 𝐻 ∈ Sℋ → ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) )
6 eleq1 ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( 𝐻 ∈ Sℋ ↔ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ∈ Sℋ ) )
7 eqid ⊢ ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ = ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩
8 xpeq1 ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( 𝐻 × 𝐻 ) = ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × 𝐻 ) )
9 xpeq2 ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × 𝐻 ) = ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) )
10 8 9 eqtrd ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( 𝐻 × 𝐻 ) = ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) )
11 10 reseq2d ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) )
12 xpeq2 ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ℂ × 𝐻 ) = ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) )
13 12 reseq2d ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ·ℎ ↾ ( ℂ × 𝐻 ) ) = ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) )
14 11 13 opeq12d ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ = ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ )
15 reseq2 ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( normℎ ↾ 𝐻 ) = ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) )
16 14 15 opeq12d ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ = ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ )
17 2 16 syl5eq ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ )
18 17 eleq1d ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ↔ ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ ∈ ( SubSp ‘ 𝑈 ) ) )
19 sseq1 ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( 𝐻 ⊆ ℋ ↔ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ⊆ ℋ ) )
20 18 19 anbi12d ⊢ ( 𝐻 = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) ↔ ( ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ ∈ ( SubSp ‘ 𝑈 ) ∧ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ⊆ ℋ ) ) )
21 xpeq1 ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ℋ × ℋ ) = ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × ℋ ) )
22 xpeq2 ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × ℋ ) = ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) )
23 21 22 eqtrd ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ℋ × ℋ ) = ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) )
24 23 reseq2d ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( +ℎ ↾ ( ℋ × ℋ ) ) = ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) )
25 xpeq2 ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ℂ × ℋ ) = ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) )
26 25 reseq2d ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ·ℎ ↾ ( ℂ × ℋ ) ) = ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) )
27 24 26 opeq12d ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ⟨ ( +ℎ ↾ ( ℋ × ℋ ) ) , ( ·ℎ ↾ ( ℂ × ℋ ) ) ⟩ = ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ )
28 reseq2 ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( normℎ ↾ ℋ ) = ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) )
29 27 28 opeq12d ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ⟨ ⟨ ( +ℎ ↾ ( ℋ × ℋ ) ) , ( ·ℎ ↾ ( ℂ × ℋ ) ) ⟩ , ( normℎ ↾ ℋ ) ⟩ = ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ )
30 29 eleq1d ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ⟨ ⟨ ( +ℎ ↾ ( ℋ × ℋ ) ) , ( ·ℎ ↾ ( ℂ × ℋ ) ) ⟩ , ( normℎ ↾ ℋ ) ⟩ ∈ ( SubSp ‘ 𝑈 ) ↔ ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ ∈ ( SubSp ‘ 𝑈 ) ) )
31 sseq1 ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ℋ ⊆ ℋ ↔ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ⊆ ℋ ) )
32 30 31 anbi12d ⊢ ( ℋ = if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) → ( ( ⟨ ⟨ ( +ℎ ↾ ( ℋ × ℋ ) ) , ( ·ℎ ↾ ( ℂ × ℋ ) ) ⟩ , ( normℎ ↾ ℋ ) ⟩ ∈ ( SubSp ‘ 𝑈 ) ∧ ℋ ⊆ ℋ ) ↔ ( ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ ∈ ( SubSp ‘ 𝑈 ) ∧ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ⊆ ℋ ) ) )
33 ax-hfvadd ⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
34 ffn ⊢ ( +ℎ : ( ℋ × ℋ ) ⟶ ℋ → +ℎ Fn ( ℋ × ℋ ) )
35 fnresdm ⊢ ( +ℎ Fn ( ℋ × ℋ ) → ( +ℎ ↾ ( ℋ × ℋ ) ) = +ℎ )
36 33 34 35 mp2b ⊢ ( +ℎ ↾ ( ℋ × ℋ ) ) = +ℎ
37 ax-hfvmul ⊢ ·ℎ : ( ℂ × ℋ ) ⟶ ℋ
38 ffn ⊢ ( ·ℎ : ( ℂ × ℋ ) ⟶ ℋ → ·ℎ Fn ( ℂ × ℋ ) )
39 fnresdm ⊢ ( ·ℎ Fn ( ℂ × ℋ ) → ( ·ℎ ↾ ( ℂ × ℋ ) ) = ·ℎ )
40 37 38 39 mp2b ⊢ ( ·ℎ ↾ ( ℂ × ℋ ) ) = ·ℎ
41 36 40 opeq12i ⊢ ⟨ ( +ℎ ↾ ( ℋ × ℋ ) ) , ( ·ℎ ↾ ( ℂ × ℋ ) ) ⟩ = ⟨ +ℎ , ·ℎ ⟩
42 normf ⊢ normℎ : ℋ ⟶ ℝ
43 ffn ⊢ ( normℎ : ℋ ⟶ ℝ → normℎ Fn ℋ )
44 fnresdm ⊢ ( normℎ Fn ℋ → ( normℎ ↾ ℋ ) = normℎ )
45 42 43 44 mp2b ⊢ ( normℎ ↾ ℋ ) = normℎ
46 41 45 opeq12i ⊢ ⟨ ⟨ ( +ℎ ↾ ( ℋ × ℋ ) ) , ( ·ℎ ↾ ( ℂ × ℋ ) ) ⟩ , ( normℎ ↾ ℋ ) ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
47 46 1 eqtr4i ⊢ ⟨ ⟨ ( +ℎ ↾ ( ℋ × ℋ ) ) , ( ·ℎ ↾ ( ℂ × ℋ ) ) ⟩ , ( normℎ ↾ ℋ ) ⟩ = 𝑈
48 1 hhnv ⊢ 𝑈 ∈ NrmCVec
49 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
50 49 sspid ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 ∈ ( SubSp ‘ 𝑈 ) )
51 48 50 ax-mp ⊢ 𝑈 ∈ ( SubSp ‘ 𝑈 )
52 47 51 eqeltri ⊢ ⟨ ⟨ ( +ℎ ↾ ( ℋ × ℋ ) ) , ( ·ℎ ↾ ( ℂ × ℋ ) ) ⟩ , ( normℎ ↾ ℋ ) ⟩ ∈ ( SubSp ‘ 𝑈 )
53 ssid ⊢ ℋ ⊆ ℋ
54 52 53 pm3.2i ⊢ ( ⟨ ⟨ ( +ℎ ↾ ( ℋ × ℋ ) ) , ( ·ℎ ↾ ( ℂ × ℋ ) ) ⟩ , ( normℎ ↾ ℋ ) ⟩ ∈ ( SubSp ‘ 𝑈 ) ∧ ℋ ⊆ ℋ )
55 20 32 54 elimhyp ⊢ ( ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ ∈ ( SubSp ‘ 𝑈 ) ∧ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ⊆ ℋ )
56 55 simpli ⊢ ⟨ ⟨ ( +ℎ ↾ ( if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ) ⟩ , ( normℎ ↾ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ) ⟩ ∈ ( SubSp ‘ 𝑈 )
57 55 simpri ⊢ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ⊆ ℋ
58 1 7 56 57 hhshsslem2 ⊢ if ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) , 𝐻 , ℋ ) ∈ Sℋ
59 6 58 dedth ⊢ ( ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) → 𝐻 ∈ Sℋ )
60 5 59 impbii ⊢ ( 𝐻 ∈ Sℋ ↔ ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝐻 ⊆ ℋ ) )