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