Step | Hyp | Ref
| Expression |
1 | | djaval.j |
. . 3
⊢ 𝐽 = ((vA‘𝐾)‘𝑊) |
2 | | djaval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
3 | 2 | djaffvalN 36422 |
. . . 4
⊢ (𝐾 ∈ 𝑉 → (vA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦)))))) |
4 | 3 | fveq1d 6193 |
. . 3
⊢ (𝐾 ∈ 𝑉 → ((vA‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦)))))‘𝑊)) |
5 | 1, 4 | syl5eq 2668 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐽 = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦)))))‘𝑊)) |
6 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
7 | | djaval.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
8 | 6, 7 | syl6eqr 2674 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = 𝑇) |
9 | 8 | pweqd 4163 |
. . . 4
⊢ (𝑤 = 𝑊 → 𝒫 ((LTrn‘𝐾)‘𝑤) = 𝒫 𝑇) |
10 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((ocA‘𝐾)‘𝑤) = ((ocA‘𝐾)‘𝑊)) |
11 | | djaval.n |
. . . . . 6
⊢ ⊥ =
((ocA‘𝐾)‘𝑊) |
12 | 10, 11 | syl6eqr 2674 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((ocA‘𝐾)‘𝑤) = ⊥ ) |
13 | 12 | fveq1d 6193 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((ocA‘𝐾)‘𝑤)‘𝑥) = ( ⊥ ‘𝑥)) |
14 | 12 | fveq1d 6193 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((ocA‘𝐾)‘𝑤)‘𝑦) = ( ⊥ ‘𝑦)) |
15 | 13, 14 | ineq12d 3815 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦)) = (( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦))) |
16 | 12, 15 | fveq12d 6197 |
. . . 4
⊢ (𝑤 = 𝑊 → (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦))) = ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) |
17 | 9, 9, 16 | mpt2eq123dv 6717 |
. . 3
⊢ (𝑤 = 𝑊 → (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦)))) = (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
18 | | eqid 2622 |
. . 3
⊢ (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦))))) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦))))) |
19 | | fvex 6201 |
. . . . . 6
⊢
((LTrn‘𝐾)‘𝑊) ∈ V |
20 | 7, 19 | eqeltri 2697 |
. . . . 5
⊢ 𝑇 ∈ V |
21 | 20 | pwex 4848 |
. . . 4
⊢ 𝒫
𝑇 ∈ V |
22 | 21, 21 | mpt2ex 7247 |
. . 3
⊢ (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) ∈
V |
23 | 17, 18, 22 | fvmpt 6282 |
. 2
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤), 𝑦 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((ocA‘𝐾)‘𝑤)‘((((ocA‘𝐾)‘𝑤)‘𝑥) ∩ (((ocA‘𝐾)‘𝑤)‘𝑦)))))‘𝑊) = (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
24 | 5, 23 | sylan9eq 2676 |
1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐽 = (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |