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

Metamath Proof Explorer

Theorem sspid

Description: A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypothesis sspid.h ⊢ 𝐻 = ( SubSp ‘ 𝑈 )
Assertion sspid ( 𝑈 ∈ NrmCVec → 𝑈 ∈ 𝐻 )

Proof

Step Hyp Ref Expression
1 sspid.h ⊢ 𝐻 = ( SubSp ‘ 𝑈 )
2 ssid ⊢ ( +𝑣 ‘ 𝑈 ) ⊆ ( +𝑣 ‘ 𝑈 )
3 ssid ⊢ ( ·𝑠OLD ‘ 𝑈 ) ⊆ ( ·𝑠OLD ‘ 𝑈 )
4 ssid ⊢ ( normCV ‘ 𝑈 ) ⊆ ( normCV ‘ 𝑈 )
5 2 3 4 3pm3.2i ⊢ ( ( +𝑣 ‘ 𝑈 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑈 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ ( normCV ‘ 𝑈 ) ⊆ ( normCV ‘ 𝑈 ) )
6 5 jctr ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑈 ∈ NrmCVec ∧ ( ( +𝑣 ‘ 𝑈 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑈 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ ( normCV ‘ 𝑈 ) ⊆ ( normCV ‘ 𝑈 ) ) ) )
7 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
8 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
9 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
10 7 7 8 8 9 9 1 isssp ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ NrmCVec ∧ ( ( +𝑣 ‘ 𝑈 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑈 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ ( normCV ‘ 𝑈 ) ⊆ ( normCV ‘ 𝑈 ) ) ) ) )
11 6 10 mpbird ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 ∈ 𝐻 )