Step | Hyp | Ref
| Expression |
1 | | ocvfval.v |
. . . 4
⊢ 𝑉 = (Base‘𝑊) |
2 | 1 | fvexi 6731 |
. . 3
⊢ 𝑉 ∈ V |
3 | 2 | elpw2 5238 |
. 2
⊢ (𝑆 ∈ 𝒫 𝑉 ↔ 𝑆 ⊆ 𝑉) |
4 | | ocvfval.i |
. . . . . 6
⊢ , =
(·𝑖‘𝑊) |
5 | | ocvfval.f |
. . . . . 6
⊢ 𝐹 = (Scalar‘𝑊) |
6 | | ocvfval.z |
. . . . . 6
⊢ 0 =
(0g‘𝐹) |
7 | | ocvfval.o |
. . . . . 6
⊢ ⊥ =
(ocv‘𝑊) |
8 | 1, 4, 5, 6, 7 | ocvfval 20628 |
. . . . 5
⊢ (𝑊 ∈ V → ⊥ =
(𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 })) |
9 | 8 | fveq1d 6719 |
. . . 4
⊢ (𝑊 ∈ V → ( ⊥
‘𝑆) = ((𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 })‘𝑆)) |
10 | | raleq 3319 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 ↔ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 )) |
11 | 10 | rabbidv 3390 |
. . . . 5
⊢ (𝑠 = 𝑆 → {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 } = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
12 | | eqid 2737 |
. . . . 5
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 }) = (𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 }) |
13 | 2 | rabex 5225 |
. . . . 5
⊢ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } ∈
V |
14 | 11, 12, 13 | fvmpt 6818 |
. . . 4
⊢ (𝑆 ∈ 𝒫 𝑉 → ((𝑠 ∈ 𝒫 𝑉 ↦ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑠 (𝑥 , 𝑦) = 0 })‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
15 | 9, 14 | sylan9eq 2798 |
. . 3
⊢ ((𝑊 ∈ V ∧ 𝑆 ∈ 𝒫 𝑉) → ( ⊥ ‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
16 | | 0fv 6756 |
. . . . 5
⊢
(∅‘𝑆) =
∅ |
17 | | fvprc 6709 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V →
(ocv‘𝑊) =
∅) |
18 | 7, 17 | syl5eq 2790 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → ⊥ =
∅) |
19 | 18 | fveq1d 6719 |
. . . . 5
⊢ (¬
𝑊 ∈ V → ( ⊥
‘𝑆) =
(∅‘𝑆)) |
20 | | ssrab2 3993 |
. . . . . 6
⊢ {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } ⊆ 𝑉 |
21 | | fvprc 6709 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V →
(Base‘𝑊) =
∅) |
22 | 1, 21 | syl5eq 2790 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → 𝑉 = ∅) |
23 | | sseq0 4314 |
. . . . . 6
⊢ (({𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } ⊆ 𝑉 ∧ 𝑉 = ∅) → {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } =
∅) |
24 | 20, 22, 23 | sylancr 590 |
. . . . 5
⊢ (¬
𝑊 ∈ V → {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 } =
∅) |
25 | 16, 19, 24 | 3eqtr4a 2804 |
. . . 4
⊢ (¬
𝑊 ∈ V → ( ⊥
‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
26 | 25 | adantr 484 |
. . 3
⊢ ((¬
𝑊 ∈ V ∧ 𝑆 ∈ 𝒫 𝑉) → ( ⊥ ‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
27 | 15, 26 | pm2.61ian 812 |
. 2
⊢ (𝑆 ∈ 𝒫 𝑉 → ( ⊥ ‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |
28 | 3, 27 | sylbir 238 |
1
⊢ (𝑆 ⊆ 𝑉 → ( ⊥ ‘𝑆) = {𝑥 ∈ 𝑉 ∣ ∀𝑦 ∈ 𝑆 (𝑥 , 𝑦) = 0 }) |