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 ⊢ H = SubSp ⁡ U
Assertion sspid ⊢ U ∈ NrmCVec → U ∈ H

Proof

Step Hyp Ref Expression
1 sspid.h ⊢ H = SubSp ⁡ U
2 ssid ⊢ + v ⁡ U ⊆ + v ⁡ U
3 ssid ⊢ ⋅ 𝑠OLD ⁡ U ⊆ ⋅ 𝑠OLD ⁡ U
4 ssid ⊢ norm CV ⁡ U ⊆ norm CV ⁡ U
5 2 3 4 3pm3.2i ⊢ + v ⁡ U ⊆ + v ⁡ U ∧ ⋅ 𝑠OLD ⁡ U ⊆ ⋅ 𝑠OLD ⁡ U ∧ norm CV ⁡ U ⊆ norm CV ⁡ U
6 5 jctr ⊢ U ∈ NrmCVec → U ∈ NrmCVec ∧ + v ⁡ U ⊆ + v ⁡ U ∧ ⋅ 𝑠OLD ⁡ U ⊆ ⋅ 𝑠OLD ⁡ U ∧ norm CV ⁡ U ⊆ norm CV ⁡ U
7 eqid ⊢ + v ⁡ U = + v ⁡ U
8 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
9 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
10 7 7 8 8 9 9 1 isssp ⊢ U ∈ NrmCVec → U ∈ H ↔ U ∈ NrmCVec ∧ + v ⁡ U ⊆ + v ⁡ U ∧ ⋅ 𝑠OLD ⁡ U ⊆ ⋅ 𝑠OLD ⁡ U ∧ norm CV ⁡ U ⊆ norm CV ⁡ U
11 6 10 mpbird ⊢ U ∈ NrmCVec → U ∈ H