Step | Hyp | Ref
| Expression |
1 | | elfvdm 6749 |
. . . . 5
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) → 𝑆 ∈ dom ⊥ ) |
2 | | n0i 4248 |
. . . . . . . . 9
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) → ¬ ( ⊥
‘𝑆) =
∅) |
3 | | ocvfval.o |
. . . . . . . . . . . 12
⊢ ⊥ =
(ocv‘𝑊) |
4 | | fvprc 6709 |
. . . . . . . . . . . 12
⊢ (¬
𝑊 ∈ V →
(ocv‘𝑊) =
∅) |
5 | 3, 4 | syl5eq 2790 |
. . . . . . . . . . 11
⊢ (¬
𝑊 ∈ V → ⊥ =
∅) |
6 | 5 | fveq1d 6719 |
. . . . . . . . . 10
⊢ (¬
𝑊 ∈ V → ( ⊥
‘𝑆) =
(∅‘𝑆)) |
7 | | 0fv 6756 |
. . . . . . . . . 10
⊢
(∅‘𝑆) =
∅ |
8 | 6, 7 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (¬
𝑊 ∈ V → ( ⊥
‘𝑆) =
∅) |
9 | 2, 8 | nsyl2 143 |
. . . . . . . 8
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) → 𝑊 ∈ V) |
10 | | ocvfval.v |
. . . . . . . . 9
⊢ 𝑉 = (Base‘𝑊) |
11 | | ocvfval.i |
. . . . . . . . 9
⊢ , =
(·𝑖‘𝑊) |
12 | | ocvfval.f |
. . . . . . . . 9
⊢ 𝐹 = (Scalar‘𝑊) |
13 | | ocvfval.z |
. . . . . . . . 9
⊢ 0 =
(0g‘𝐹) |
14 | 10, 11, 12, 13, 3 | ocvfval 20628 |
. . . . . . . 8
⊢ (𝑊 ∈ V → ⊥ =
(𝑠 ∈ 𝒫 𝑉 ↦ {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑠 (𝑦 , 𝑥) = 0 })) |
15 | 9, 14 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) → ⊥ = (𝑠 ∈ 𝒫 𝑉 ↦ {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑠 (𝑦 , 𝑥) = 0 })) |
16 | 15 | dmeqd 5774 |
. . . . . 6
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) → dom ⊥ = dom (𝑠 ∈ 𝒫 𝑉 ↦ {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑠 (𝑦 , 𝑥) = 0 })) |
17 | 10 | fvexi 6731 |
. . . . . . . 8
⊢ 𝑉 ∈ V |
18 | 17 | rabex 5225 |
. . . . . . 7
⊢ {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑠 (𝑦 , 𝑥) = 0 } ∈
V |
19 | | eqid 2737 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝑉 ↦ {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑠 (𝑦 , 𝑥) = 0 }) = (𝑠 ∈ 𝒫 𝑉 ↦ {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑠 (𝑦 , 𝑥) = 0 }) |
20 | 18, 19 | dmmpti 6522 |
. . . . . 6
⊢ dom
(𝑠 ∈ 𝒫 𝑉 ↦ {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑠 (𝑦 , 𝑥) = 0 }) = 𝒫 𝑉 |
21 | 16, 20 | eqtrdi 2794 |
. . . . 5
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) → dom ⊥ = 𝒫 𝑉) |
22 | 1, 21 | eleqtrd 2840 |
. . . 4
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) → 𝑆 ∈ 𝒫 𝑉) |
23 | 22 | elpwid 4524 |
. . 3
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) → 𝑆 ⊆ 𝑉) |
24 | 10, 11, 12, 13, 3 | ocvval 20629 |
. . . . 5
⊢ (𝑆 ⊆ 𝑉 → ( ⊥ ‘𝑆) = {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑆 (𝑦 , 𝑥) = 0 }) |
25 | 24 | eleq2d 2823 |
. . . 4
⊢ (𝑆 ⊆ 𝑉 → (𝐴 ∈ ( ⊥ ‘𝑆) ↔ 𝐴 ∈ {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑆 (𝑦 , 𝑥) = 0 })) |
26 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑦 , 𝑥) = (𝐴 , 𝑥)) |
27 | 26 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝑦 , 𝑥) = 0 ↔ (𝐴 , 𝑥) = 0 )) |
28 | 27 | ralbidv 3118 |
. . . . 5
⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝑆 (𝑦 , 𝑥) = 0 ↔ ∀𝑥 ∈ 𝑆 (𝐴 , 𝑥) = 0 )) |
29 | 28 | elrab 3602 |
. . . 4
⊢ (𝐴 ∈ {𝑦 ∈ 𝑉 ∣ ∀𝑥 ∈ 𝑆 (𝑦 , 𝑥) = 0 } ↔ (𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (𝐴 , 𝑥) = 0 )) |
30 | 25, 29 | bitrdi 290 |
. . 3
⊢ (𝑆 ⊆ 𝑉 → (𝐴 ∈ ( ⊥ ‘𝑆) ↔ (𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (𝐴 , 𝑥) = 0 ))) |
31 | 23, 30 | biadanii 822 |
. 2
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) ↔ (𝑆 ⊆ 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (𝐴 , 𝑥) = 0 ))) |
32 | | 3anass 1097 |
. 2
⊢ ((𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (𝐴 , 𝑥) = 0 ) ↔ (𝑆 ⊆ 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (𝐴 , 𝑥) = 0 ))) |
33 | 31, 32 | bitr4i 281 |
1
⊢ (𝐴 ∈ ( ⊥ ‘𝑆) ↔ (𝑆 ⊆ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑆 (𝐴 , 𝑥) = 0 )) |