Step | Hyp | Ref
| Expression |
1 | | ocvfval.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
2 | | fvex 6201 |
. . . 4
⊢
(Base‘𝑊)
∈ V |
3 | 1, 2 | eqeltri 2697 |
. . 3
⊢ 𝑉 ∈ V |
4 | 3 | elpw2 4828 |
. 2
⊢ (𝑆 ∈ 𝒫 𝑉 ↔ 𝑆 ⊆ 𝑉) |
5 | | ocvfval.i |
. . . . . 6
⊢ , =
(·𝑖‘𝑊) |
6 | | ocvfval.f |
. . . . . 6
⊢ 𝐹 = (Scalar‘𝑊) |
7 | | ocvfval.z |
. . . . . 6
⊢ 0 =
(0g‘𝐹) |
8 | | ocvfval.o |
. . . . . 6
⊢ ⊥ =
(ocv‘𝑊) |
9 | 1, 5, 6, 7, 8 | ocvfval 20010 |
. . . . 5
⊢ (𝑊 ∈ V → ⊥ =
(𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 })) |
10 | 9 | fveq1d 6193 |
. . . 4
⊢ (𝑊 ∈ V → ( ⊥
‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 })‘𝑆)) |
11 | | raleq 3138 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 ↔ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 )) |
12 | 11 | rabbidv 3189 |
. . . . 5
⊢ (𝑠 = 𝑆 → {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 } = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
13 | | eqid 2622 |
. . . . 5
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 }) = (𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 }) |
14 | 3 | rabex 4813 |
. . . . 5
⊢ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } ∈
V |
15 | 12, 13, 14 | fvmpt 6282 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝑉 → ((𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 })‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
16 | 10, 15 | sylan9eq 2676 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝑆 ∈ 𝒫 𝑉) → ( ⊥ ‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
17 | | 0fv 6227 |
. . . . 5
⊢
(∅‘𝑆) =
∅ |
18 | | fvprc 6185 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V →
(ocv‘𝑊) =
∅) |
19 | 8, 18 | syl5eq 2668 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → ⊥ =
∅) |
20 | 19 | fveq1d 6193 |
. . . . 5
⊢ (¬
𝑊 ∈ V → ( ⊥
‘𝑆) =
(∅‘𝑆)) |
21 | | ssrab2 3687 |
. . . . . 6
⊢ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } ⊆ 𝑉 |
22 | | fvprc 6185 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V →
(Base‘𝑊) =
∅) |
23 | 1, 22 | syl5eq 2668 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → 𝑉 = ∅) |
24 | | sseq0 3975 |
. . . . . 6
⊢ (({𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } ⊆ 𝑉 ∧ 𝑉 = ∅) → {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } =
∅) |
25 | 21, 23, 24 | sylancr 695 |
. . . . 5
⊢ (¬
𝑊 ∈ V → {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } =
∅) |
26 | 17, 20, 25 | 3eqtr4a 2682 |
. . . 4
⊢ (¬
𝑊 ∈ V → ( ⊥
‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
27 | 26 | adantr 481 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝑆 ∈ 𝒫 𝑉) → ( ⊥ ‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
28 | 16, 27 | pm2.61ian 831 |
. 2
⊢ (𝑆 ∈ 𝒫 𝑉 → ( ⊥ ‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
29 | 4, 28 | sylbir 225 |
1
⊢ (𝑆 ⊆ 𝑉 → ( ⊥ ‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |