Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . 5
⊢ (𝑥 = 𝑇 → 𝑥 = 𝑇) |
2 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝑇 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑇)) |
3 | 1, 2 | oveq12d 6567 |
. . . 4
⊢ (𝑥 = 𝑇 → (𝑥𝑃( ⊥ ‘𝑥)) = (𝑇𝑃( ⊥ ‘𝑇))) |
4 | 3 | eleq1d 2672 |
. . 3
⊢ (𝑥 = 𝑇 → ((𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑𝑚 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)) ∈ (𝑉 ↑𝑚 𝑉))) |
5 | | pjfval.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
6 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑊)
∈ V |
7 | 5, 6 | eqeltri 2684 |
. . . 4
⊢ 𝑉 ∈ V |
8 | 7, 7 | elmap 7772 |
. . 3
⊢ ((𝑇𝑃( ⊥ ‘𝑇)) ∈ (𝑉 ↑𝑚 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉) |
9 | 4, 8 | syl6bb 275 |
. 2
⊢ (𝑥 = 𝑇 → ((𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑𝑚 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉)) |
10 | | cnvin 5459 |
. . . . . . 7
⊢ ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ◡(V × (𝑉 ↑𝑚 𝑉))) |
11 | | cnvxp 5470 |
. . . . . . . 8
⊢ ◡(V × (𝑉 ↑𝑚 𝑉)) = ((𝑉 ↑𝑚 𝑉) × V) |
12 | 11 | ineq2i 3773 |
. . . . . . 7
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ◡(V × (𝑉 ↑𝑚 𝑉))) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ((𝑉 ↑𝑚 𝑉) × V)) |
13 | 10, 12 | eqtri 2632 |
. . . . . 6
⊢ ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ((𝑉 ↑𝑚 𝑉) × V)) |
14 | | pjfval.l |
. . . . . . . 8
⊢ 𝐿 = (LSubSp‘𝑊) |
15 | | pjfval.o |
. . . . . . . 8
⊢ ⊥ =
(ocv‘𝑊) |
16 | | pjfval.p |
. . . . . . . 8
⊢ 𝑃 = (proj1‘𝑊) |
17 | | pjfval.k |
. . . . . . . 8
⊢ 𝐾 = (proj‘𝑊) |
18 | 5, 14, 15, 16, 17 | pjfval 19869 |
. . . . . . 7
⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) |
19 | 18 | cnveqi 5219 |
. . . . . 6
⊢ ◡𝐾 = ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) |
20 | | df-res 5050 |
. . . . . 6
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑𝑚 𝑉)) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ((𝑉 ↑𝑚 𝑉) × V)) |
21 | 13, 19, 20 | 3eqtr4i 2642 |
. . . . 5
⊢ ◡𝐾 = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑𝑚 𝑉)) |
22 | 21 | rneqi 5273 |
. . . 4
⊢ ran ◡𝐾 = ran (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑𝑚 𝑉)) |
23 | | dfdm4 5238 |
. . . 4
⊢ dom 𝐾 = ran ◡𝐾 |
24 | | df-ima 5051 |
. . . 4
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑𝑚 𝑉)) = ran (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑𝑚 𝑉)) |
25 | 22, 23, 24 | 3eqtr4i 2642 |
. . 3
⊢ dom 𝐾 = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑𝑚 𝑉)) |
26 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) |
27 | 26 | mptpreima 5545 |
. . 3
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑𝑚 𝑉)) = {𝑥 ∈ 𝐿 ∣ (𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑𝑚 𝑉)} |
28 | 25, 27 | eqtri 2632 |
. 2
⊢ dom 𝐾 = {𝑥 ∈ 𝐿 ∣ (𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑𝑚 𝑉)} |
29 | 9, 28 | elrab2 3333 |
1
⊢ (𝑇 ∈ dom 𝐾 ↔ (𝑇 ∈ 𝐿 ∧ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉)) |