Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . 5
⊢ (𝑥 = 𝑇 → 𝑥 = 𝑇) |
2 | | fveq2 6191 |
. . . . 5
⊢ (𝑥 = 𝑇 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑇)) |
3 | 1, 2 | oveq12d 6668 |
. . . 4
⊢ (𝑥 = 𝑇 → (𝑥𝑃( ⊥ ‘𝑥)) = (𝑇𝑃( ⊥ ‘𝑇))) |
4 | 3 | eleq1d 2686 |
. . 3
⊢ (𝑥 = 𝑇 → ((𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑𝑚 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)) ∈ (𝑉 ↑𝑚 𝑉))) |
5 | | pjfval.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
6 | | fvex 6201 |
. . . . 5
⊢
(Base‘𝑊)
∈ V |
7 | 5, 6 | eqeltri 2697 |
. . . 4
⊢ 𝑉 ∈ V |
8 | 7, 7 | elmap 7886 |
. . 3
⊢ ((𝑇𝑃( ⊥ ‘𝑇)) ∈ (𝑉 ↑𝑚 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉) |
9 | 4, 8 | syl6bb 276 |
. 2
⊢ (𝑥 = 𝑇 → ((𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑𝑚 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉)) |
10 | | cnvin 5540 |
. . . . . . 7
⊢ ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ◡(V × (𝑉 ↑𝑚 𝑉))) |
11 | | cnvxp 5551 |
. . . . . . . 8
⊢ ◡(V × (𝑉 ↑𝑚 𝑉)) = ((𝑉 ↑𝑚 𝑉) × V) |
12 | 11 | ineq2i 3811 |
. . . . . . 7
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ◡(V × (𝑉 ↑𝑚 𝑉))) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ((𝑉 ↑𝑚 𝑉) × V)) |
13 | 10, 12 | eqtri 2644 |
. . . . . 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 20050 |
. . . . . . 7
⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) |
19 | 18 | cnveqi 5297 |
. . . . . 6
⊢ ◡𝐾 = ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) |
20 | | df-res 5126 |
. . . . . 6
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑𝑚 𝑉)) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ((𝑉 ↑𝑚 𝑉) × V)) |
21 | 13, 19, 20 | 3eqtr4i 2654 |
. . . . 5
⊢ ◡𝐾 = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑𝑚 𝑉)) |
22 | 21 | rneqi 5352 |
. . . 4
⊢ ran ◡𝐾 = ran (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑𝑚 𝑉)) |
23 | | dfdm4 5316 |
. . . 4
⊢ dom 𝐾 = ran ◡𝐾 |
24 | | df-ima 5127 |
. . . 4
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑𝑚 𝑉)) = ran (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑𝑚 𝑉)) |
25 | 22, 23, 24 | 3eqtr4i 2654 |
. . 3
⊢ dom 𝐾 = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑𝑚 𝑉)) |
26 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) |
27 | 26 | mptpreima 5628 |
. . 3
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑𝑚 𝑉)) = {𝑥 ∈ 𝐿 ∣ (𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑𝑚 𝑉)} |
28 | 25, 27 | eqtri 2644 |
. 2
⊢ dom 𝐾 = {𝑥 ∈ 𝐿 ∣ (𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑𝑚 𝑉)} |
29 | 9, 28 | elrab2 3366 |
1
⊢ (𝑇 ∈ dom 𝐾 ↔ (𝑇 ∈ 𝐿 ∧ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉)) |