Step | Hyp | Ref
| Expression |
1 | | pjfval.k |
. 2
⊢ 𝐾 = (proj‘𝑊) |
2 | | fveq2 6496 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = (LSubSp‘𝑊)) |
3 | | pjfval.l |
. . . . . . 7
⊢ 𝐿 = (LSubSp‘𝑊) |
4 | 2, 3 | syl6eqr 2825 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (LSubSp‘𝑤) = 𝐿) |
5 | | fveq2 6496 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (proj1‘𝑤) =
(proj1‘𝑊)) |
6 | | pjfval.p |
. . . . . . . 8
⊢ 𝑃 = (proj1‘𝑊) |
7 | 5, 6 | syl6eqr 2825 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (proj1‘𝑤) = 𝑃) |
8 | | eqidd 2772 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → 𝑥 = 𝑥) |
9 | | fveq2 6496 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (ocv‘𝑤) = (ocv‘𝑊)) |
10 | | pjfval.o |
. . . . . . . . 9
⊢ ⊥ =
(ocv‘𝑊) |
11 | 9, 10 | syl6eqr 2825 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (ocv‘𝑤) = ⊥ ) |
12 | 11 | fveq1d 6498 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((ocv‘𝑤)‘𝑥) = ( ⊥ ‘𝑥)) |
13 | 7, 8, 12 | oveq123d 6995 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (𝑥(proj1‘𝑤)((ocv‘𝑤)‘𝑥)) = (𝑥𝑃( ⊥ ‘𝑥))) |
14 | 4, 13 | mpteq12dv 5008 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑥 ∈ (LSubSp‘𝑤) ↦ (𝑥(proj1‘𝑤)((ocv‘𝑤)‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥)))) |
15 | | fveq2 6496 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
16 | | pjfval.v |
. . . . . . . 8
⊢ 𝑉 = (Base‘𝑊) |
17 | 15, 16 | syl6eqr 2825 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝑉) |
18 | 17, 17 | oveq12d 6992 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((Base‘𝑤) ↑𝑚
(Base‘𝑤)) = (𝑉 ↑𝑚
𝑉)) |
19 | 18 | xpeq2d 5433 |
. . . . 5
⊢ (𝑤 = 𝑊 → (V × ((Base‘𝑤) ↑𝑚
(Base‘𝑤))) = (V
× (𝑉
↑𝑚 𝑉))) |
20 | 14, 19 | ineq12d 4071 |
. . . 4
⊢ (𝑤 = 𝑊 → ((𝑥 ∈ (LSubSp‘𝑤) ↦ (𝑥(proj1‘𝑤)((ocv‘𝑤)‘𝑥))) ∩ (V × ((Base‘𝑤) ↑𝑚
(Base‘𝑤)))) = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉)))) |
21 | | df-pj 20564 |
. . . 4
⊢ proj =
(𝑤 ∈ V ↦ ((𝑥 ∈ (LSubSp‘𝑤) ↦ (𝑥(proj1‘𝑤)((ocv‘𝑤)‘𝑥))) ∩ (V × ((Base‘𝑤) ↑𝑚
(Base‘𝑤))))) |
22 | 3 | fvexi 6510 |
. . . . . . 7
⊢ 𝐿 ∈ V |
23 | 22 | inex1 5074 |
. . . . . 6
⊢ (𝐿 ∩ V) ∈
V |
24 | | ovex 7006 |
. . . . . . 7
⊢ (𝑉 ↑𝑚
𝑉) ∈
V |
25 | 24 | inex2 5075 |
. . . . . 6
⊢ (V ∩
(𝑉
↑𝑚 𝑉)) ∈ V |
26 | 23, 25 | xpex 7291 |
. . . . 5
⊢ ((𝐿 ∩ V) × (V ∩
(𝑉
↑𝑚 𝑉))) ∈ V |
27 | | eqid 2771 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) |
28 | | ovexd 7008 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐿 → (𝑥𝑃( ⊥ ‘𝑥)) ∈ V) |
29 | 27, 28 | fmpti 6697 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))):𝐿⟶V |
30 | | fssxp 6360 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))):𝐿⟶V → (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ⊆ (𝐿 × V)) |
31 | | ssrin 4091 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ⊆ (𝐿 × V) → ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) ⊆ ((𝐿 × V) ∩ (V ×
(𝑉
↑𝑚 𝑉)))) |
32 | 29, 30, 31 | mp2b 10 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) ⊆ ((𝐿 × V) ∩ (V ×
(𝑉
↑𝑚 𝑉))) |
33 | | inxp 5549 |
. . . . . 6
⊢ ((𝐿 × V) ∩ (V ×
(𝑉
↑𝑚 𝑉))) = ((𝐿 ∩ V) × (V ∩ (𝑉 ↑𝑚
𝑉))) |
34 | 32, 33 | sseqtri 3886 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) ⊆ ((𝐿 ∩ V) × (V ∩
(𝑉
↑𝑚 𝑉))) |
35 | 26, 34 | ssexi 5078 |
. . . 4
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) ∈
V |
36 | 20, 21, 35 | fvmpt 6593 |
. . 3
⊢ (𝑊 ∈ V →
(proj‘𝑊) = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉)))) |
37 | | fvprc 6489 |
. . . 4
⊢ (¬
𝑊 ∈ V →
(proj‘𝑊) =
∅) |
38 | | inss1 4086 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) |
39 | | fvprc 6489 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V →
(LSubSp‘𝑊) =
∅) |
40 | 3, 39 | syl5eq 2819 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V → 𝐿 = ∅) |
41 | 40 | mpteq1d 5012 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = (𝑥 ∈ ∅ ↦ (𝑥𝑃( ⊥ ‘𝑥)))) |
42 | | mpt0 6317 |
. . . . . 6
⊢ (𝑥 ∈ ∅ ↦ (𝑥𝑃( ⊥ ‘𝑥))) = ∅ |
43 | 41, 42 | syl6eq 2823 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = ∅) |
44 | | sseq0 4233 |
. . . . 5
⊢ ((((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∧ (𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) = ∅) → ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) =
∅) |
45 | 38, 43, 44 | sylancr 579 |
. . . 4
⊢ (¬
𝑊 ∈ V → ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) =
∅) |
46 | 37, 45 | eqtr4d 2810 |
. . 3
⊢ (¬
𝑊 ∈ V →
(proj‘𝑊) = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉)))) |
47 | 36, 46 | pm2.61i 177 |
. 2
⊢
(proj‘𝑊) =
((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) |
48 | 1, 47 | eqtri 2795 |
1
⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥𝑃( ⊥ ‘𝑥))) ∩ (V × (𝑉 ↑𝑚
𝑉))) |