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