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