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 → 𝑈𝐻 )