Step |
Hyp |
Ref |
Expression |
1 |
|
pjpm.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
pjpm.l |
⊢ 𝐿 = ( LSubSp ‘ 𝑊 ) |
3 |
|
pjpm.k |
⊢ 𝐾 = ( proj ‘ 𝑊 ) |
4 |
|
eqid |
⊢ ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 ) |
5 |
|
eqid |
⊢ ( proj1 ‘ 𝑊 ) = ( proj1 ‘ 𝑊 ) |
6 |
1 2 4 5 3
|
pjfval |
⊢ 𝐾 = ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) |
7 |
|
inss1 |
⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ⊆ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) |
8 |
6 7
|
eqsstri |
⊢ 𝐾 ⊆ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) |
9 |
|
funmpt |
⊢ Fun ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) |
10 |
|
funss |
⊢ ( 𝐾 ⊆ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) → ( Fun ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) → Fun 𝐾 ) ) |
11 |
8 9 10
|
mp2 |
⊢ Fun 𝐾 |
12 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) |
13 |
|
ovexd |
⊢ ( 𝑥 ∈ 𝐿 → ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ∈ V ) |
14 |
12 13
|
fmpti |
⊢ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) : 𝐿 ⟶ V |
15 |
|
fssxp |
⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) : 𝐿 ⟶ V → ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ⊆ ( 𝐿 × V ) ) |
16 |
|
ssrin |
⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ⊆ ( 𝐿 × V ) → ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ⊆ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ) |
17 |
14 15 16
|
mp2b |
⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 ( proj1 ‘ 𝑊 ) ( ( ocv ‘ 𝑊 ) ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) ⊆ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) |
18 |
6 17
|
eqsstri |
⊢ 𝐾 ⊆ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) |
19 |
|
inxp |
⊢ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) = ( ( 𝐿 ∩ V ) × ( V ∩ ( 𝑉 ↑m 𝑉 ) ) ) |
20 |
|
inv1 |
⊢ ( 𝐿 ∩ V ) = 𝐿 |
21 |
|
incom |
⊢ ( V ∩ ( 𝑉 ↑m 𝑉 ) ) = ( ( 𝑉 ↑m 𝑉 ) ∩ V ) |
22 |
|
inv1 |
⊢ ( ( 𝑉 ↑m 𝑉 ) ∩ V ) = ( 𝑉 ↑m 𝑉 ) |
23 |
21 22
|
eqtri |
⊢ ( V ∩ ( 𝑉 ↑m 𝑉 ) ) = ( 𝑉 ↑m 𝑉 ) |
24 |
20 23
|
xpeq12i |
⊢ ( ( 𝐿 ∩ V ) × ( V ∩ ( 𝑉 ↑m 𝑉 ) ) ) = ( 𝐿 × ( 𝑉 ↑m 𝑉 ) ) |
25 |
19 24
|
eqtri |
⊢ ( ( 𝐿 × V ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) = ( 𝐿 × ( 𝑉 ↑m 𝑉 ) ) |
26 |
18 25
|
sseqtri |
⊢ 𝐾 ⊆ ( 𝐿 × ( 𝑉 ↑m 𝑉 ) ) |
27 |
|
ovex |
⊢ ( 𝑉 ↑m 𝑉 ) ∈ V |
28 |
2
|
fvexi |
⊢ 𝐿 ∈ V |
29 |
27 28
|
elpm |
⊢ ( 𝐾 ∈ ( ( 𝑉 ↑m 𝑉 ) ↑pm 𝐿 ) ↔ ( Fun 𝐾 ∧ 𝐾 ⊆ ( 𝐿 × ( 𝑉 ↑m 𝑉 ) ) ) ) |
30 |
11 26 29
|
mpbir2an |
⊢ 𝐾 ∈ ( ( 𝑉 ↑m 𝑉 ) ↑pm 𝐿 ) |