Step | Hyp | Ref
| Expression |
1 | | sspval.h |
. 2
⊢ 𝐻 = (SubSp‘𝑈) |
2 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = ( +𝑣
‘𝑈)) |
3 | | sspval.g |
. . . . . . 7
⊢ 𝐺 = ( +𝑣
‘𝑈) |
4 | 2, 3 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = 𝐺) |
5 | 4 | sseq2d 3633 |
. . . . 5
⊢ (𝑢 = 𝑈 → (( +𝑣
‘𝑤) ⊆ (
+𝑣 ‘𝑢) ↔ ( +𝑣 ‘𝑤) ⊆ 𝐺)) |
6 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → (
·𝑠OLD ‘𝑢) = ( ·𝑠OLD
‘𝑈)) |
7 | | sspval.s |
. . . . . . 7
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
8 | 6, 7 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑢 = 𝑈 → (
·𝑠OLD ‘𝑢) = 𝑆) |
9 | 8 | sseq2d 3633 |
. . . . 5
⊢ (𝑢 = 𝑈 → ((
·𝑠OLD ‘𝑤) ⊆ (
·𝑠OLD ‘𝑢) ↔ (
·𝑠OLD ‘𝑤) ⊆ 𝑆)) |
10 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑢 = 𝑈 → (normCV‘𝑢) =
(normCV‘𝑈)) |
11 | | sspval.n |
. . . . . . 7
⊢ 𝑁 =
(normCV‘𝑈) |
12 | 10, 11 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑢 = 𝑈 → (normCV‘𝑢) = 𝑁) |
13 | 12 | sseq2d 3633 |
. . . . 5
⊢ (𝑢 = 𝑈 → ((normCV‘𝑤) ⊆
(normCV‘𝑢)
↔ (normCV‘𝑤) ⊆ 𝑁)) |
14 | 5, 9, 13 | 3anbi123d 1399 |
. . . 4
⊢ (𝑢 = 𝑈 → ((( +𝑣
‘𝑤) ⊆ (
+𝑣 ‘𝑢) ∧ (
·𝑠OLD ‘𝑤) ⊆ (
·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆
(normCV‘𝑢)) ↔ (( +𝑣
‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁))) |
15 | 14 | rabbidv 3189 |
. . 3
⊢ (𝑢 = 𝑈 → {𝑤 ∈ NrmCVec ∣ ((
+𝑣 ‘𝑤) ⊆ ( +𝑣
‘𝑢) ∧ (
·𝑠OLD ‘𝑤) ⊆ (
·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆
(normCV‘𝑢))} = {𝑤 ∈ NrmCVec ∣ ((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁)}) |
16 | | df-ssp 27577 |
. . 3
⊢ SubSp =
(𝑢 ∈ NrmCVec ↦
{𝑤 ∈ NrmCVec ∣
(( +𝑣 ‘𝑤) ⊆ ( +𝑣
‘𝑢) ∧ (
·𝑠OLD ‘𝑤) ⊆ (
·𝑠OLD ‘𝑢) ∧ (normCV‘𝑤) ⊆
(normCV‘𝑢))}) |
17 | | fvex 6201 |
. . . . . . . 8
⊢ (
+𝑣 ‘𝑈) ∈ V |
18 | 3, 17 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐺 ∈ V |
19 | 18 | pwex 4848 |
. . . . . 6
⊢ 𝒫
𝐺 ∈ V |
20 | | fvex 6201 |
. . . . . . . 8
⊢ (
·𝑠OLD ‘𝑈) ∈ V |
21 | 7, 20 | eqeltri 2697 |
. . . . . . 7
⊢ 𝑆 ∈ V |
22 | 21 | pwex 4848 |
. . . . . 6
⊢ 𝒫
𝑆 ∈ V |
23 | 19, 22 | xpex 6962 |
. . . . 5
⊢
(𝒫 𝐺 ×
𝒫 𝑆) ∈
V |
24 | | fvex 6201 |
. . . . . . 7
⊢
(normCV‘𝑈) ∈ V |
25 | 11, 24 | eqeltri 2697 |
. . . . . 6
⊢ 𝑁 ∈ V |
26 | 25 | pwex 4848 |
. . . . 5
⊢ 𝒫
𝑁 ∈ V |
27 | 23, 26 | xpex 6962 |
. . . 4
⊢
((𝒫 𝐺
× 𝒫 𝑆)
× 𝒫 𝑁) ∈
V |
28 | | rabss 3679 |
. . . . 5
⊢ ({𝑤 ∈ NrmCVec ∣ ((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁)} ⊆ ((𝒫 𝐺 × 𝒫 𝑆) × 𝒫 𝑁) ↔ ∀𝑤 ∈ NrmCVec ((( +𝑣
‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁) → 𝑤 ∈ ((𝒫 𝐺 × 𝒫 𝑆) × 𝒫 𝑁))) |
29 | | fvex 6201 |
. . . . . . . . . 10
⊢ (
+𝑣 ‘𝑤) ∈ V |
30 | 29 | elpw 4164 |
. . . . . . . . 9
⊢ ((
+𝑣 ‘𝑤) ∈ 𝒫 𝐺 ↔ ( +𝑣 ‘𝑤) ⊆ 𝐺) |
31 | | fvex 6201 |
. . . . . . . . . 10
⊢ (
·𝑠OLD ‘𝑤) ∈ V |
32 | 31 | elpw 4164 |
. . . . . . . . 9
⊢ ((
·𝑠OLD ‘𝑤) ∈ 𝒫 𝑆 ↔ (
·𝑠OLD ‘𝑤) ⊆ 𝑆) |
33 | | opelxpi 5148 |
. . . . . . . . 9
⊢ (((
+𝑣 ‘𝑤) ∈ 𝒫 𝐺 ∧ (
·𝑠OLD ‘𝑤) ∈ 𝒫 𝑆) → 〈( +𝑣
‘𝑤), (
·𝑠OLD ‘𝑤)〉 ∈ (𝒫 𝐺 × 𝒫 𝑆)) |
34 | 30, 32, 33 | syl2anbr 497 |
. . . . . . . 8
⊢ (((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆) → 〈( +𝑣
‘𝑤), (
·𝑠OLD ‘𝑤)〉 ∈ (𝒫 𝐺 × 𝒫 𝑆)) |
35 | | fvex 6201 |
. . . . . . . . . 10
⊢
(normCV‘𝑤) ∈ V |
36 | 35 | elpw 4164 |
. . . . . . . . 9
⊢
((normCV‘𝑤) ∈ 𝒫 𝑁 ↔ (normCV‘𝑤) ⊆ 𝑁) |
37 | 36 | biimpri 218 |
. . . . . . . 8
⊢
((normCV‘𝑤) ⊆ 𝑁 → (normCV‘𝑤) ∈ 𝒫 𝑁) |
38 | | opelxpi 5148 |
. . . . . . . 8
⊢ ((〈(
+𝑣 ‘𝑤), ( ·𝑠OLD
‘𝑤)〉 ∈
(𝒫 𝐺 ×
𝒫 𝑆) ∧
(normCV‘𝑤)
∈ 𝒫 𝑁) →
〈〈( +𝑣 ‘𝑤), ( ·𝑠OLD
‘𝑤)〉,
(normCV‘𝑤)〉 ∈ ((𝒫 𝐺 × 𝒫 𝑆) × 𝒫 𝑁)) |
39 | 34, 37, 38 | syl2an 494 |
. . . . . . 7
⊢ ((((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆) ∧ (normCV‘𝑤) ⊆ 𝑁) → 〈〈( +𝑣
‘𝑤), (
·𝑠OLD ‘𝑤)〉, (normCV‘𝑤)〉 ∈ ((𝒫 𝐺 × 𝒫 𝑆) × 𝒫 𝑁)) |
40 | 39 | 3impa 1259 |
. . . . . 6
⊢ (((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁) → 〈〈( +𝑣
‘𝑤), (
·𝑠OLD ‘𝑤)〉, (normCV‘𝑤)〉 ∈ ((𝒫 𝐺 × 𝒫 𝑆) × 𝒫 𝑁)) |
41 | | eqid 2622 |
. . . . . . . 8
⊢ (
+𝑣 ‘𝑤) = ( +𝑣 ‘𝑤) |
42 | | eqid 2622 |
. . . . . . . 8
⊢ (
·𝑠OLD ‘𝑤) = ( ·𝑠OLD
‘𝑤) |
43 | | eqid 2622 |
. . . . . . . 8
⊢
(normCV‘𝑤) = (normCV‘𝑤) |
44 | 41, 42, 43 | nvop 27531 |
. . . . . . 7
⊢ (𝑤 ∈ NrmCVec → 𝑤 = 〈〈(
+𝑣 ‘𝑤), ( ·𝑠OLD
‘𝑤)〉,
(normCV‘𝑤)〉) |
45 | 44 | eleq1d 2686 |
. . . . . 6
⊢ (𝑤 ∈ NrmCVec → (𝑤 ∈ ((𝒫 𝐺 × 𝒫 𝑆) × 𝒫 𝑁) ↔ 〈〈(
+𝑣 ‘𝑤), ( ·𝑠OLD
‘𝑤)〉,
(normCV‘𝑤)〉 ∈ ((𝒫 𝐺 × 𝒫 𝑆) × 𝒫 𝑁))) |
46 | 40, 45 | syl5ibr 236 |
. . . . 5
⊢ (𝑤 ∈ NrmCVec → (((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁) → 𝑤 ∈ ((𝒫 𝐺 × 𝒫 𝑆) × 𝒫 𝑁))) |
47 | 28, 46 | mprgbir 2927 |
. . . 4
⊢ {𝑤 ∈ NrmCVec ∣ ((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁)} ⊆ ((𝒫 𝐺 × 𝒫 𝑆) × 𝒫 𝑁) |
48 | 27, 47 | ssexi 4803 |
. . 3
⊢ {𝑤 ∈ NrmCVec ∣ ((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁)} ∈ V |
49 | 15, 16, 48 | fvmpt 6282 |
. 2
⊢ (𝑈 ∈ NrmCVec →
(SubSp‘𝑈) = {𝑤 ∈ NrmCVec ∣ ((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁)}) |
50 | 1, 49 | syl5eq 2668 |
1
⊢ (𝑈 ∈ NrmCVec → 𝐻 = {𝑤 ∈ NrmCVec ∣ ((
+𝑣 ‘𝑤) ⊆ 𝐺 ∧ (
·𝑠OLD ‘𝑤) ⊆ 𝑆 ∧ (normCV‘𝑤) ⊆ 𝑁)}) |