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	syl5eq	⊢ ( 𝐻 = 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 )