Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . 5
⊢ (𝑥 = 𝑇 → 𝑥 = 𝑇) |
2 | | fveq2 6717 |
. . . . 5
⊢ (𝑥 = 𝑇 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑇)) |
3 | 1, 2 | oveq12d 7231 |
. . . 4
⊢ (𝑥 = 𝑇 → (𝑥𝑃( ⊥ ‘𝑥)) = (𝑇𝑃( ⊥ ‘𝑇))) |
4 | 3 | eleq1d 2822 |
. . 3
⊢ (𝑥 = 𝑇 → ((𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑m 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)) ∈ (𝑉 ↑m 𝑉))) |
5 | | pjfval.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
6 | 5 | fvexi 6731 |
. . . 4
⊢ 𝑉 ∈ V |
7 | 6, 6 | elmap 8552 |
. . 3
⊢ ((𝑇𝑃( ⊥ ‘𝑇)) ∈ (𝑉 ↑m 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉) |
8 | 4, 7 | bitrdi 290 |
. 2
⊢ (𝑥 = 𝑇 → ((𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑m 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉)) |
9 | | cnvin 6008 |
. . . . . . 7
⊢ ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ◡(V × (𝑉 ↑m 𝑉))) |
10 | | cnvxp 6020 |
. . . . . . . 8
⊢ ◡(V × (𝑉 ↑m 𝑉)) = ((𝑉 ↑m 𝑉) × V) |
11 | 10 | ineq2i 4124 |
. . . . . . 7
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ◡(V × (𝑉 ↑m 𝑉))) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ((𝑉 ↑m 𝑉) × V)) |
12 | 9, 11 | eqtri 2765 |
. . . . . 6
⊢ ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ((𝑉 ↑m 𝑉) × V)) |
13 | | pjfval.l |
. . . . . . . 8
⊢ 𝐿 = (LSubSp‘𝑊) |
14 | | pjfval.o |
. . . . . . . 8
⊢ ⊥ =
(ocv‘𝑊) |
15 | | pjfval.p |
. . . . . . . 8
⊢ 𝑃 = (proj1‘𝑊) |
16 | | pjfval.k |
. . . . . . . 8
⊢ 𝐾 = (proj‘𝑊) |
17 | 5, 13, 14, 15, 16 | pjfval 20668 |
. . . . . . 7
⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) |
18 | 17 | cnveqi 5743 |
. . . . . 6
⊢ ◡𝐾 = ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) |
19 | | df-res 5563 |
. . . . . 6
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑m 𝑉)) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ((𝑉 ↑m 𝑉) × V)) |
20 | 12, 18, 19 | 3eqtr4i 2775 |
. . . . 5
⊢ ◡𝐾 = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑m 𝑉)) |
21 | 20 | rneqi 5806 |
. . . 4
⊢ ran ◡𝐾 = ran (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑m 𝑉)) |
22 | | dfdm4 5764 |
. . . 4
⊢ dom 𝐾 = ran ◡𝐾 |
23 | | df-ima 5564 |
. . . 4
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑m 𝑉)) = ran (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑m 𝑉)) |
24 | 21, 22, 23 | 3eqtr4i 2775 |
. . 3
⊢ dom 𝐾 = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑m 𝑉)) |
25 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) |
26 | 25 | mptpreima 6101 |
. . 3
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑m 𝑉)) = {𝑥 ∈ 𝐿 ∣ (𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑m 𝑉)} |
27 | 24, 26 | eqtri 2765 |
. 2
⊢ dom 𝐾 = {𝑥 ∈ 𝐿 ∣ (𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑m 𝑉)} |
28 | 8, 27 | elrab2 3605 |
1
⊢ (𝑇 ∈ dom 𝐾 ↔ (𝑇 ∈ 𝐿 ∧ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉)) |