Step | Hyp | Ref
| Expression |
1 | | pjpm.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
2 | | pjpm.l |
. . . . 5
⊢ 𝐿 = (LSubSp‘𝑊) |
3 | | eqid 2610 |
. . . . 5
⊢
(ocv‘𝑊) =
(ocv‘𝑊) |
4 | | eqid 2610 |
. . . . 5
⊢
(proj1‘𝑊) = (proj1‘𝑊) |
5 | | pjpm.k |
. . . . 5
⊢ 𝐾 = (proj‘𝑊) |
6 | 1, 2, 3, 4, 5 | pjfval 19869 |
. . . 4
⊢ 𝐾 = ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑𝑚 𝑉))) |
7 | | inss1 3795 |
. . . 4
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑𝑚 𝑉))) ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
8 | 6, 7 | eqsstri 3598 |
. . 3
⊢ 𝐾 ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
9 | | funmpt 5840 |
. . 3
⊢ Fun
(𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
10 | | funss 5822 |
. . 3
⊢ (𝐾 ⊆ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) → (Fun (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) → Fun 𝐾)) |
11 | 8, 9, 10 | mp2 9 |
. 2
⊢ Fun 𝐾 |
12 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) = (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) |
13 | | ovex 6577 |
. . . . . . 7
⊢ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥)) ∈ V |
14 | 13 | a1i 11 |
. . . . . 6
⊢ (𝑥 ∈ 𝐿 → (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥)) ∈ V) |
15 | 12, 14 | fmpti 6291 |
. . . . 5
⊢ (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))):𝐿⟶V |
16 | | fssxp 5973 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))):𝐿⟶V → (𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ⊆ (𝐿 × V)) |
17 | | ssrin 3800 |
. . . . 5
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ⊆ (𝐿 × V) → ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑𝑚 𝑉))) ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑𝑚
𝑉)))) |
18 | 15, 16, 17 | mp2b 10 |
. . . 4
⊢ ((𝑥 ∈ 𝐿 ↦ (𝑥(proj1‘𝑊)((ocv‘𝑊)‘𝑥))) ∩ (V × (𝑉 ↑𝑚 𝑉))) ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑𝑚
𝑉))) |
19 | 6, 18 | eqsstri 3598 |
. . 3
⊢ 𝐾 ⊆ ((𝐿 × V) ∩ (V × (𝑉 ↑𝑚
𝑉))) |
20 | | inxp 5176 |
. . . 4
⊢ ((𝐿 × V) ∩ (V ×
(𝑉
↑𝑚 𝑉))) = ((𝐿 ∩ V) × (V ∩ (𝑉 ↑𝑚
𝑉))) |
21 | | inv1 3922 |
. . . . 5
⊢ (𝐿 ∩ V) = 𝐿 |
22 | | incom 3767 |
. . . . . 6
⊢ (V ∩
(𝑉
↑𝑚 𝑉)) = ((𝑉 ↑𝑚 𝑉) ∩ V) |
23 | | inv1 3922 |
. . . . . 6
⊢ ((𝑉 ↑𝑚
𝑉) ∩ V) = (𝑉 ↑𝑚
𝑉) |
24 | 22, 23 | eqtri 2632 |
. . . . 5
⊢ (V ∩
(𝑉
↑𝑚 𝑉)) = (𝑉 ↑𝑚 𝑉) |
25 | 21, 24 | xpeq12i 5061 |
. . . 4
⊢ ((𝐿 ∩ V) × (V ∩
(𝑉
↑𝑚 𝑉))) = (𝐿 × (𝑉 ↑𝑚 𝑉)) |
26 | 20, 25 | eqtri 2632 |
. . 3
⊢ ((𝐿 × V) ∩ (V ×
(𝑉
↑𝑚 𝑉))) = (𝐿 × (𝑉 ↑𝑚 𝑉)) |
27 | 19, 26 | sseqtri 3600 |
. 2
⊢ 𝐾 ⊆ (𝐿 × (𝑉 ↑𝑚 𝑉)) |
28 | | ovex 6577 |
. . 3
⊢ (𝑉 ↑𝑚
𝑉) ∈
V |
29 | | fvex 6113 |
. . . 4
⊢
(LSubSp‘𝑊)
∈ V |
30 | 2, 29 | eqeltri 2684 |
. . 3
⊢ 𝐿 ∈ V |
31 | 28, 30 | elpm 7774 |
. 2
⊢ (𝐾 ∈ ((𝑉 ↑𝑚 𝑉) ↑pm
𝐿) ↔ (Fun 𝐾 ∧ 𝐾 ⊆ (𝐿 × (𝑉 ↑𝑚 𝑉)))) |
32 | 11, 27, 31 | mpbir2an 957 |
1
⊢ 𝐾 ∈ ((𝑉 ↑𝑚 𝑉) ↑pm
𝐿) |