Step | Hyp | Ref
| Expression |
1 | | pjfval.k |
. 2
⊢ 𝐾 = (proj‘𝑊) |
2 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = (LSubSp‘𝑊)) |
3 | | pjfval.l |
. . . . . . 7
⊢ 𝐿 = (LSubSp‘𝑊) |
4 | 2, 3 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = 𝐿) |
5 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (proj1‘𝑤) =
(proj1‘𝑊)) |
6 | | pjfval.p |
. . . . . . . 8
⊢ 𝑃 = (proj1‘𝑊) |
7 | 5, 6 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (proj1‘𝑤) = 𝑃) |
8 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥) |
9 | | fveq2 6717 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (ocv‘𝑤) = (ocv‘𝑊)) |
10 | | pjfval.o |
. . . . . . . . 9
⊢ ⊥ =
(ocv‘𝑊) |
11 | 9, 10 | eqtr4di 2796 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (ocv‘𝑤) = ⊥ ) |
12 | 11 | fveq1d 6719 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((ocv‘𝑤)‘𝑥) = ( ⊥ ‘𝑥)) |
13 | 7, 8, 12 | oveq123d 7234 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑥(proj1‘𝑤)((ocv‘𝑤)‘𝑥)) = (𝑥𝑃( ⊥ ‘𝑥))) |
14 | 4, 13 | mpteq12dv 5140 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (LSubSp‘𝑤) ↦ (𝑥(proj1‘𝑤)((ocv‘𝑤)‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥)))) |
15 | | fveq2 6717 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
16 | | pjfval.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) |
17 | 15, 16 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
18 | 17, 17 | oveq12d 7231 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((Base‘𝑤) ↑m (Base‘𝑤)) = (𝑉 ↑m 𝑉)) |
19 | 18 | xpeq2d 5581 |
. . . . 5
⊢ (𝑤 = 𝑊 → (V × ((Base‘𝑤) ↑m
(Base‘𝑤))) = (V
× (𝑉
↑m 𝑉))) |
20 | 14, 19 | ineq12d 4128 |
. . . 4
⊢ (𝑤 = 𝑊 → ((𝑥 ∈ (LSubSp‘𝑤) ↦ (𝑥(proj1‘𝑤)((ocv‘𝑤)‘𝑥))) ∩ (V × ((Base‘𝑤) ↑m
(Base‘𝑤)))) = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉)))) |
21 | | df-pj 20665 |
. . . 4
⊢ proj =
(𝑤 ∈ V ↦ ((𝑥 ∈ (LSubSp‘𝑤) ↦ (𝑥(proj1‘𝑤)((ocv‘𝑤)‘𝑥))) ∩ (V × ((Base‘𝑤) ↑m
(Base‘𝑤))))) |
22 | 3 | fvexi 6731 |
. . . . . . 7
⊢ 𝐿 ∈ V |
23 | 22 | inex1 5210 |
. . . . . 6
⊢ (𝐿 ∩ V) ∈
V |
24 | | ovex 7246 |
. . . . . . 7
⊢ (𝑉 ↑m 𝑉) ∈ V |
25 | 24 | inex2 5211 |
. . . . . 6
⊢ (V ∩
(𝑉 ↑m 𝑉)) ∈ V |
26 | 23, 25 | xpex 7538 |
. . . . 5
⊢ ((𝐿 ∩ V) × (V ∩
(𝑉 ↑m 𝑉))) ∈ V |
27 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) |
28 | | ovexd 7248 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐿 → (𝑥𝑃( ⊥ ‘𝑥)) ∈ V) |
29 | 27, 28 | fmpti 6929 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))):𝐿⟶V |
30 | | fssxp 6573 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))):𝐿⟶V → (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ⊆ (𝐿 × V)) |
31 | | ssrin 4148 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ⊆ (𝐿 × V) → ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑m 𝑉)))) |
32 | 29, 30, 31 | mp2b 10 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑m 𝑉))) |
33 | | inxp 5701 |
. . . . . 6
⊢ ((𝐿 × V) ∩ (V ×
(𝑉 ↑m 𝑉))) = ((𝐿 ∩ V) × (V ∩ (𝑉 ↑m 𝑉))) |
34 | 32, 33 | sseqtri 3937 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) ⊆ ((𝐿 ∩ V) × (V ∩ (𝑉 ↑m 𝑉))) |
35 | 26, 34 | ssexi 5215 |
. . . 4
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) ∈ V |
36 | 20, 21, 35 | fvmpt 6818 |
. . 3
⊢ (𝑊 ∈ V →
(proj‘𝑊) = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉)))) |
37 | | fvprc 6709 |
. . . 4
⊢ (¬
𝑊 ∈ V →
(proj‘𝑊) =
∅) |
38 | | inss1 4143 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) |
39 | | fvprc 6709 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V →
(LSubSp‘𝑊) =
∅) |
40 | 3, 39 | syl5eq 2790 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V → 𝐿 = ∅) |
41 | 40 | mpteq1d 5144 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = (𝑥 ∈ ∅ ↦ (𝑥𝑃( ⊥ ‘𝑥)))) |
42 | | mpt0 6520 |
. . . . . 6
⊢ (𝑥 ∈ ∅ ↦ (𝑥𝑃( ⊥ ‘𝑥))) = ∅ |
43 | 41, 42 | eqtrdi 2794 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = ∅) |
44 | | sseq0 4314 |
. . . . 5
⊢ ((((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∧ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = ∅) → ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) = ∅) |
45 | 38, 43, 44 | sylancr 590 |
. . . 4
⊢ (¬
𝑊 ∈ V → ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) = ∅) |
46 | 37, 45 | eqtr4d 2780 |
. . 3
⊢ (¬
𝑊 ∈ V →
(proj‘𝑊) = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉)))) |
47 | 36, 46 | pm2.61i 185 |
. 2
⊢
(proj‘𝑊) =
((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) |
48 | 1, 47 | eqtri 2765 |
1
⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑m 𝑉))) |