Step |
Hyp |
Ref |
Expression |
1 |
|
isssp.g |
⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) |
2 |
|
isssp.f |
⊢ 𝐹 = ( +𝑣 ‘ 𝑊 ) |
3 |
|
isssp.s |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
4 |
|
isssp.r |
⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑊 ) |
5 |
|
isssp.n |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
6 |
|
isssp.m |
⊢ 𝑀 = ( normCV ‘ 𝑊 ) |
7 |
|
isssp.h |
⊢ 𝐻 = ( SubSp ‘ 𝑈 ) |
8 |
1 3 5 7
|
sspval |
⊢ ( 𝑈 ∈ NrmCVec → 𝐻 = { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ) |
9 |
8
|
eleq2d |
⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ 𝑊 ∈ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ) ) |
10 |
|
fveq2 |
⊢ ( 𝑤 = 𝑊 → ( +𝑣 ‘ 𝑤 ) = ( +𝑣 ‘ 𝑊 ) ) |
11 |
10 2
|
eqtr4di |
⊢ ( 𝑤 = 𝑊 → ( +𝑣 ‘ 𝑤 ) = 𝐹 ) |
12 |
11
|
sseq1d |
⊢ ( 𝑤 = 𝑊 → ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ↔ 𝐹 ⊆ 𝐺 ) ) |
13 |
|
fveq2 |
⊢ ( 𝑤 = 𝑊 → ( ·𝑠OLD ‘ 𝑤 ) = ( ·𝑠OLD ‘ 𝑊 ) ) |
14 |
13 4
|
eqtr4di |
⊢ ( 𝑤 = 𝑊 → ( ·𝑠OLD ‘ 𝑤 ) = 𝑅 ) |
15 |
14
|
sseq1d |
⊢ ( 𝑤 = 𝑊 → ( ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ↔ 𝑅 ⊆ 𝑆 ) ) |
16 |
|
fveq2 |
⊢ ( 𝑤 = 𝑊 → ( normCV ‘ 𝑤 ) = ( normCV ‘ 𝑊 ) ) |
17 |
16 6
|
eqtr4di |
⊢ ( 𝑤 = 𝑊 → ( normCV ‘ 𝑤 ) = 𝑀 ) |
18 |
17
|
sseq1d |
⊢ ( 𝑤 = 𝑊 → ( ( normCV ‘ 𝑤 ) ⊆ 𝑁 ↔ 𝑀 ⊆ 𝑁 ) ) |
19 |
12 15 18
|
3anbi123d |
⊢ ( 𝑤 = 𝑊 → ( ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) ↔ ( 𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁 ) ) ) |
20 |
19
|
elrab |
⊢ ( 𝑊 ∈ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ↔ ( 𝑊 ∈ NrmCVec ∧ ( 𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁 ) ) ) |
21 |
9 20
|
bitrdi |
⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ NrmCVec ∧ ( 𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁 ) ) ) ) |