Step |
Hyp |
Ref |
Expression |
1 |
|
pjfval.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
pjfval.l |
⊢ 𝐿 = ( LSubSp ‘ 𝑊 ) |
3 |
|
pjfval.o |
⊢ ⊥ = ( ocv ‘ 𝑊 ) |
4 |
|
pjfval.p |
⊢ 𝑃 = ( proj1 ‘ 𝑊 ) |
5 |
|
pjfval.k |
⊢ 𝐾 = ( proj ‘ 𝑊 ) |
6 |
|
id |
⊢ ( 𝑥 = 𝑇 → 𝑥 = 𝑇 ) |
7 |
|
fveq2 |
⊢ ( 𝑥 = 𝑇 → ( ⊥ ‘ 𝑥 ) = ( ⊥ ‘ 𝑇 ) ) |
8 |
6 7
|
oveq12d |
⊢ ( 𝑥 = 𝑇 → ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) = ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) ) |
9 |
8
|
eleq1d |
⊢ ( 𝑥 = 𝑇 → ( ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ∈ ( 𝑉 ↑m 𝑉 ) ↔ ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) ∈ ( 𝑉 ↑m 𝑉 ) ) ) |
10 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
11 |
10 10
|
elmap |
⊢ ( ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) ∈ ( 𝑉 ↑m 𝑉 ) ↔ ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) |
12 |
9 11
|
bitrdi |
⊢ ( 𝑥 = 𝑇 → ( ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ∈ ( 𝑉 ↑m 𝑉 ) ↔ ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) ) |
13 |
|
cnvin |
⊢ ◡ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) = ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ◡ ( V × ( 𝑉 ↑m 𝑉 ) ) ) |
14 |
|
cnvxp |
⊢ ◡ ( V × ( 𝑉 ↑m 𝑉 ) ) = ( ( 𝑉 ↑m 𝑉 ) × V ) |
15 |
14
|
ineq2i |
⊢ ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ◡ ( V × ( 𝑉 ↑m 𝑉 ) ) ) = ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( ( 𝑉 ↑m 𝑉 ) × V ) ) |
16 |
13 15
|
eqtri |
⊢ ◡ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) = ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( ( 𝑉 ↑m 𝑉 ) × V ) ) |
17 |
1 2 3 4 5
|
pjfval |
⊢ 𝐾 = ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) |
18 |
17
|
cnveqi |
⊢ ◡ 𝐾 = ◡ ( ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( 𝑉 ↑m 𝑉 ) ) ) |
19 |
|
df-res |
⊢ ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ↾ ( 𝑉 ↑m 𝑉 ) ) = ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( ( 𝑉 ↑m 𝑉 ) × V ) ) |
20 |
16 18 19
|
3eqtr4i |
⊢ ◡ 𝐾 = ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ↾ ( 𝑉 ↑m 𝑉 ) ) |
21 |
20
|
rneqi |
⊢ ran ◡ 𝐾 = ran ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ↾ ( 𝑉 ↑m 𝑉 ) ) |
22 |
|
dfdm4 |
⊢ dom 𝐾 = ran ◡ 𝐾 |
23 |
|
df-ima |
⊢ ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) “ ( 𝑉 ↑m 𝑉 ) ) = ran ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ↾ ( 𝑉 ↑m 𝑉 ) ) |
24 |
21 22 23
|
3eqtr4i |
⊢ dom 𝐾 = ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) “ ( 𝑉 ↑m 𝑉 ) ) |
25 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) |
26 |
25
|
mptpreima |
⊢ ( ◡ ( 𝑥 ∈ 𝐿 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) “ ( 𝑉 ↑m 𝑉 ) ) = { 𝑥 ∈ 𝐿 ∣ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ∈ ( 𝑉 ↑m 𝑉 ) } |
27 |
24 26
|
eqtri |
⊢ dom 𝐾 = { 𝑥 ∈ 𝐿 ∣ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ∈ ( 𝑉 ↑m 𝑉 ) } |
28 |
12 27
|
elrab2 |
⊢ ( 𝑇 ∈ dom 𝐾 ↔ ( 𝑇 ∈ 𝐿 ∧ ( 𝑇 𝑃 ( ⊥ ‘ 𝑇 ) ) : 𝑉 ⟶ 𝑉 ) ) |