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

Metamath Proof Explorer

Theorem hhssnvt

Description: Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis hhssnvt.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
Assertion hhssnvt ( 𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec )

Proof

Step Hyp Ref Expression
1 hhssnvt.1 ⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
2 xpeq1 ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ( 𝐻 × 𝐻 ) = ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × 𝐻 ) )
3 xpeq2 ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × 𝐻 ) = ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) )
4 2 3 eqtrd ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ( 𝐻 × 𝐻 ) = ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) )
5 4 reseq2d ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) = ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) )
6 xpeq2 ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ( ℂ × 𝐻 ) = ( ℂ × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) )
7 6 reseq2d ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ( ·ℎ ↾ ( ℂ × 𝐻 ) ) = ( ·ℎ ↾ ( ℂ × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) )
8 5 7 opeq12d ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ = ⟨ ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) ⟩ )
9 reseq2 ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ( normℎ ↾ 𝐻 ) = ( normℎ ↾ if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) )
10 8 9 opeq12d ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩ = ⟨ ⟨ ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) ⟩ , ( normℎ ↾ if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ⟩ )
11 1 10 eqtrid ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) ⟩ , ( normℎ ↾ if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ⟩ )
12 11 eleq1d ⊢ ( 𝐻 = if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) → ( 𝑊 ∈ NrmCVec ↔ ⟨ ⟨ ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) ⟩ , ( normℎ ↾ if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ⟩ ∈ NrmCVec ) )
13 eqid ⊢ ⟨ ⟨ ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) ⟩ , ( normℎ ↾ if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ⟩ = ⟨ ⟨ ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) ⟩ , ( normℎ ↾ if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ⟩
14 h0elsh ⊢ 0ℋ ∈ Sℋ
15 14 elimel ⊢ if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ∈ Sℋ
16 13 15 hhssnv ⊢ ⟨ ⟨ ( +ℎ ↾ ( if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) , ( ·ℎ ↾ ( ℂ × if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ) ⟩ , ( normℎ ↾ if ( 𝐻 ∈ Sℋ , 𝐻 , 0ℋ ) ) ⟩ ∈ NrmCVec
17 12 16 dedth ⊢ ( 𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec )