| Step | Hyp | Ref
| Expression |
| 1 | | id 22 |
. . . . 5
⊢ (𝑥 = 𝑇 → 𝑥 = 𝑇) |
| 2 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = 𝑇 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑇)) |
| 3 | 1, 2 | oveq12d 7449 |
. . . 4
⊢ (𝑥 = 𝑇 → (𝑥𝑃( ⊥ ‘𝑥)) = (𝑇𝑃( ⊥ ‘𝑇))) |
| 4 | 3 | eleq1d 2826 |
. . 3
⊢ (𝑥 = 𝑇 → ((𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑m 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)) ∈ (𝑉 ↑m 𝑉))) |
| 5 | | pjfval.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
| 6 | 5 | fvexi 6920 |
. . . 4
⊢ 𝑉 ∈ V |
| 7 | 6, 6 | elmap 8911 |
. . 3
⊢ ((𝑇𝑃( ⊥ ‘𝑇)) ∈ (𝑉 ↑m 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉) |
| 8 | 4, 7 | bitrdi 287 |
. 2
⊢ (𝑥 = 𝑇 → ((𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑m 𝑉) ↔ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉)) |
| 9 | | cnvin 6164 |
. . . . . . 7
⊢ ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ◡(V × (𝑉 ↑m 𝑉))) |
| 10 | | cnvxp 6177 |
. . . . . . . 8
⊢ ◡(V × (𝑉 ↑m 𝑉)) = ((𝑉 ↑m 𝑉) × V) |
| 11 | 10 | ineq2i 4217 |
. . . . . . 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 21726 |
. . . . . . 7
⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) |
| 18 | 17 | cnveqi 5885 |
. . . . . 6
⊢ ◡𝐾 = ◡((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) |
| 19 | | df-res 5697 |
. . . . . 6
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑m 𝑉)) = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ ((𝑉 ↑m 𝑉) × V)) |
| 20 | 12, 18, 19 | 3eqtr4i 2775 |
. . . . 5
⊢ ◡𝐾 = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑m 𝑉)) |
| 21 | 20 | rneqi 5948 |
. . . 4
⊢ ran ◡𝐾 = ran (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑m 𝑉)) |
| 22 | | dfdm4 5906 |
. . . 4
⊢ dom 𝐾 = ran ◡𝐾 |
| 23 | | df-ima 5698 |
. . . 4
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑m 𝑉)) = ran (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ↾ (𝑉 ↑m 𝑉)) |
| 24 | 21, 22, 23 | 3eqtr4i 2775 |
. . 3
⊢ dom 𝐾 = (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑m 𝑉)) |
| 25 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) |
| 26 | 25 | mptpreima 6258 |
. . 3
⊢ (◡(𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) “ (𝑉 ↑m 𝑉)) = {𝑥 ∈ 𝐿 ∣ (𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑m 𝑉)} |
| 27 | 24, 26 | eqtri 2765 |
. 2
⊢ dom 𝐾 = {𝑥 ∈ 𝐿 ∣ (𝑥𝑃( ⊥ ‘𝑥)) ∈ (𝑉 ↑m 𝑉)} |
| 28 | 8, 27 | elrab2 3695 |
1
⊢ (𝑇 ∈ dom 𝐾 ↔ (𝑇 ∈ 𝐿 ∧ (𝑇𝑃( ⊥ ‘𝑇)):𝑉⟶𝑉)) |