Step |
Hyp |
Ref |
Expression |
1 |
|
pjfval2.o |
⊢ ⊥ = ( ocv ‘ 𝑊 ) |
2 |
|
pjfval2.p |
⊢ 𝑃 = ( proj1 ‘ 𝑊 ) |
3 |
|
pjfval2.k |
⊢ 𝐾 = ( proj ‘ 𝑊 ) |
4 |
|
df-mpt |
⊢ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) } |
5 |
|
df-xp |
⊢ ( V × ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) } |
6 |
4 5
|
ineq12i |
⊢ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) = ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) } ∩ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) } ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
8 |
|
eqid |
⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 ) |
9 |
7 8 1 2 3
|
pjfval |
⊢ 𝐾 = ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∩ ( V × ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) |
10 |
7 8 1 2 3
|
pjdm |
⊢ ( 𝑥 ∈ dom 𝐾 ↔ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) ) ) |
11 |
|
eleq1 |
⊢ ( 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) → ( 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ↔ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) |
12 |
|
fvex |
⊢ ( Base ‘ 𝑊 ) ∈ V |
13 |
12 12
|
elmap |
⊢ ( ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ↔ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) ) |
14 |
11 13
|
bitr2di |
⊢ ( 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) → ( ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) ↔ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) |
15 |
14
|
anbi2d |
⊢ ( 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) → ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) ) ↔ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) ) |
16 |
10 15
|
syl5bb |
⊢ ( 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) → ( 𝑥 ∈ dom 𝐾 ↔ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) ) |
17 |
16
|
pm5.32ri |
⊢ ( ( 𝑥 ∈ dom 𝐾 ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ) |
18 |
|
an32 |
⊢ ( ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) |
19 |
|
vex |
⊢ 𝑥 ∈ V |
20 |
19
|
biantrur |
⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ↔ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) |
21 |
20
|
anbi2i |
⊢ ( ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ↔ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) ) |
22 |
17 18 21
|
3bitri |
⊢ ( ( 𝑥 ∈ dom 𝐾 ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ↔ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) ) |
23 |
22
|
opabbii |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ dom 𝐾 ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) } |
24 |
|
df-mpt |
⊢ ( 𝑥 ∈ dom 𝐾 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ dom 𝐾 ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) } |
25 |
|
inopab |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) } ∩ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) } ) = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) ) } |
26 |
23 24 25
|
3eqtr4i |
⊢ ( 𝑥 ∈ dom 𝐾 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) = ( { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑦 = ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) } ∩ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ ( ( Base ‘ 𝑊 ) ↑m ( Base ‘ 𝑊 ) ) ) } ) |
27 |
6 9 26
|
3eqtr4i |
⊢ 𝐾 = ( 𝑥 ∈ dom 𝐾 ↦ ( 𝑥 𝑃 ( ⊥ ‘ 𝑥 ) ) ) |