Step |
Hyp |
Ref |
Expression |
1 |
|
sspval.g |
⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) |
2 |
|
sspval.s |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
3 |
|
sspval.n |
⊢ 𝑁 = ( normCV ‘ 𝑈 ) |
4 |
|
sspval.h |
⊢ 𝐻 = ( SubSp ‘ 𝑈 ) |
5 |
|
fveq2 |
⊢ ( 𝑢 = 𝑈 → ( +𝑣 ‘ 𝑢 ) = ( +𝑣 ‘ 𝑈 ) ) |
6 |
5 1
|
eqtr4di |
⊢ ( 𝑢 = 𝑈 → ( +𝑣 ‘ 𝑢 ) = 𝐺 ) |
7 |
6
|
sseq2d |
⊢ ( 𝑢 = 𝑈 → ( ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 ) ↔ ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ) ) |
8 |
|
fveq2 |
⊢ ( 𝑢 = 𝑈 → ( ·𝑠OLD ‘ 𝑢 ) = ( ·𝑠OLD ‘ 𝑈 ) ) |
9 |
8 2
|
eqtr4di |
⊢ ( 𝑢 = 𝑈 → ( ·𝑠OLD ‘ 𝑢 ) = 𝑆 ) |
10 |
9
|
sseq2d |
⊢ ( 𝑢 = 𝑈 → ( ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 ) ↔ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ) ) |
11 |
|
fveq2 |
⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = ( normCV ‘ 𝑈 ) ) |
12 |
11 3
|
eqtr4di |
⊢ ( 𝑢 = 𝑈 → ( normCV ‘ 𝑢 ) = 𝑁 ) |
13 |
12
|
sseq2d |
⊢ ( 𝑢 = 𝑈 → ( ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 ) ↔ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) ) |
14 |
7 10 13
|
3anbi123d |
⊢ ( 𝑢 = 𝑈 → ( ( ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 ) ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 ) ∧ ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 ) ) ↔ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) ) ) |
15 |
14
|
rabbidv |
⊢ ( 𝑢 = 𝑈 → { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 ) ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 ) ∧ ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 ) ) } = { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ) |
16 |
|
df-ssp |
⊢ SubSp = ( 𝑢 ∈ NrmCVec ↦ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ ( +𝑣 ‘ 𝑢 ) ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ ( ·𝑠OLD ‘ 𝑢 ) ∧ ( normCV ‘ 𝑤 ) ⊆ ( normCV ‘ 𝑢 ) ) } ) |
17 |
1
|
fvexi |
⊢ 𝐺 ∈ V |
18 |
17
|
pwex |
⊢ 𝒫 𝐺 ∈ V |
19 |
2
|
fvexi |
⊢ 𝑆 ∈ V |
20 |
19
|
pwex |
⊢ 𝒫 𝑆 ∈ V |
21 |
18 20
|
xpex |
⊢ ( 𝒫 𝐺 × 𝒫 𝑆 ) ∈ V |
22 |
3
|
fvexi |
⊢ 𝑁 ∈ V |
23 |
22
|
pwex |
⊢ 𝒫 𝑁 ∈ V |
24 |
21 23
|
xpex |
⊢ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ∈ V |
25 |
|
rabss |
⊢ ( { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ⊆ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ↔ ∀ 𝑤 ∈ NrmCVec ( ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) → 𝑤 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ) ) |
26 |
|
fvex |
⊢ ( +𝑣 ‘ 𝑤 ) ∈ V |
27 |
26
|
elpw |
⊢ ( ( +𝑣 ‘ 𝑤 ) ∈ 𝒫 𝐺 ↔ ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ) |
28 |
|
fvex |
⊢ ( ·𝑠OLD ‘ 𝑤 ) ∈ V |
29 |
28
|
elpw |
⊢ ( ( ·𝑠OLD ‘ 𝑤 ) ∈ 𝒫 𝑆 ↔ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ) |
30 |
|
opelxpi |
⊢ ( ( ( +𝑣 ‘ 𝑤 ) ∈ 𝒫 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ∈ 𝒫 𝑆 ) → 〈 ( +𝑣 ‘ 𝑤 ) , ( ·𝑠OLD ‘ 𝑤 ) 〉 ∈ ( 𝒫 𝐺 × 𝒫 𝑆 ) ) |
31 |
27 29 30
|
syl2anbr |
⊢ ( ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ) → 〈 ( +𝑣 ‘ 𝑤 ) , ( ·𝑠OLD ‘ 𝑤 ) 〉 ∈ ( 𝒫 𝐺 × 𝒫 𝑆 ) ) |
32 |
|
fvex |
⊢ ( normCV ‘ 𝑤 ) ∈ V |
33 |
32
|
elpw |
⊢ ( ( normCV ‘ 𝑤 ) ∈ 𝒫 𝑁 ↔ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) |
34 |
33
|
biimpri |
⊢ ( ( normCV ‘ 𝑤 ) ⊆ 𝑁 → ( normCV ‘ 𝑤 ) ∈ 𝒫 𝑁 ) |
35 |
|
opelxpi |
⊢ ( ( 〈 ( +𝑣 ‘ 𝑤 ) , ( ·𝑠OLD ‘ 𝑤 ) 〉 ∈ ( 𝒫 𝐺 × 𝒫 𝑆 ) ∧ ( normCV ‘ 𝑤 ) ∈ 𝒫 𝑁 ) → 〈 〈 ( +𝑣 ‘ 𝑤 ) , ( ·𝑠OLD ‘ 𝑤 ) 〉 , ( normCV ‘ 𝑤 ) 〉 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ) |
36 |
31 34 35
|
syl2an |
⊢ ( ( ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ) ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) → 〈 〈 ( +𝑣 ‘ 𝑤 ) , ( ·𝑠OLD ‘ 𝑤 ) 〉 , ( normCV ‘ 𝑤 ) 〉 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ) |
37 |
36
|
3impa |
⊢ ( ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) → 〈 〈 ( +𝑣 ‘ 𝑤 ) , ( ·𝑠OLD ‘ 𝑤 ) 〉 , ( normCV ‘ 𝑤 ) 〉 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ) |
38 |
|
eqid |
⊢ ( +𝑣 ‘ 𝑤 ) = ( +𝑣 ‘ 𝑤 ) |
39 |
|
eqid |
⊢ ( ·𝑠OLD ‘ 𝑤 ) = ( ·𝑠OLD ‘ 𝑤 ) |
40 |
|
eqid |
⊢ ( normCV ‘ 𝑤 ) = ( normCV ‘ 𝑤 ) |
41 |
38 39 40
|
nvop |
⊢ ( 𝑤 ∈ NrmCVec → 𝑤 = 〈 〈 ( +𝑣 ‘ 𝑤 ) , ( ·𝑠OLD ‘ 𝑤 ) 〉 , ( normCV ‘ 𝑤 ) 〉 ) |
42 |
41
|
eleq1d |
⊢ ( 𝑤 ∈ NrmCVec → ( 𝑤 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ↔ 〈 〈 ( +𝑣 ‘ 𝑤 ) , ( ·𝑠OLD ‘ 𝑤 ) 〉 , ( normCV ‘ 𝑤 ) 〉 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ) ) |
43 |
37 42
|
syl5ibr |
⊢ ( 𝑤 ∈ NrmCVec → ( ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) → 𝑤 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ) ) |
44 |
25 43
|
mprgbir |
⊢ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ⊆ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) |
45 |
24 44
|
ssexi |
⊢ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ∈ V |
46 |
15 16 45
|
fvmpt |
⊢ ( 𝑈 ∈ NrmCVec → ( SubSp ‘ 𝑈 ) = { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ) |
47 |
4 46
|
syl5eq |
⊢ ( 𝑈 ∈ NrmCVec → 𝐻 = { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ) |