Step | Hyp | Ref
| Expression |
1 | | djhval.j |
. . 3
⊢ ∨ =
((joinH‘𝐾)‘𝑊) |
2 | | djhval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
3 | 2 | djhffval 36685 |
. . . 4
⊢ (𝐾 ∈ 𝑋 → (joinH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))) |
4 | 3 | fveq1d 6193 |
. . 3
⊢ (𝐾 ∈ 𝑋 → ((joinH‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))‘𝑊)) |
5 | 1, 4 | syl5eq 2668 |
. 2
⊢ (𝐾 ∈ 𝑋 → ∨ = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))‘𝑊)) |
6 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((DVecH‘𝐾)‘𝑤) = ((DVecH‘𝐾)‘𝑊)) |
7 | 6 | fveq2d 6195 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘((DVecH‘𝐾)‘𝑤)) = (Base‘((DVecH‘𝐾)‘𝑊))) |
8 | | djhval.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
9 | | djhval.u |
. . . . . . . 8
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
10 | 9 | fveq2i 6194 |
. . . . . . 7
⊢
(Base‘𝑈) =
(Base‘((DVecH‘𝐾)‘𝑊)) |
11 | 8, 10 | eqtri 2644 |
. . . . . 6
⊢ 𝑉 =
(Base‘((DVecH‘𝐾)‘𝑊)) |
12 | 7, 11 | syl6eqr 2674 |
. . . . 5
⊢ (𝑤 = 𝑊 → (Base‘((DVecH‘𝐾)‘𝑤)) = 𝑉) |
13 | 12 | pweqd 4163 |
. . . 4
⊢ (𝑤 = 𝑊 → 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) = 𝒫 𝑉) |
14 | | fveq2 6191 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((ocH‘𝐾)‘𝑤) = ((ocH‘𝐾)‘𝑊)) |
15 | | djhval.o |
. . . . . 6
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
16 | 14, 15 | syl6eqr 2674 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((ocH‘𝐾)‘𝑤) = ⊥ ) |
17 | 16 | fveq1d 6193 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((ocH‘𝐾)‘𝑤)‘𝑥) = ( ⊥ ‘𝑥)) |
18 | 16 | fveq1d 6193 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((ocH‘𝐾)‘𝑤)‘𝑦) = ( ⊥ ‘𝑦)) |
19 | 17, 18 | ineq12d 3815 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)) = (( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦))) |
20 | 16, 19 | fveq12d 6197 |
. . . 4
⊢ (𝑤 = 𝑊 → (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦))) = ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) |
21 | 13, 13, 20 | mpt2eq123dv 6717 |
. . 3
⊢ (𝑤 = 𝑊 → (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))) = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
22 | | eqid 2622 |
. . 3
⊢ (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦))))) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦))))) |
23 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝑈)
∈ V |
24 | 8, 23 | eqeltri 2697 |
. . . . 5
⊢ 𝑉 ∈ V |
25 | 24 | pwex 4848 |
. . . 4
⊢ 𝒫
𝑉 ∈ V |
26 | 25, 25 | mpt2ex 7247 |
. . 3
⊢ (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) ∈
V |
27 | 21, 22, 26 | fvmpt 6282 |
. 2
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))‘𝑊) = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
28 | 5, 27 | sylan9eq 2676 |
1
⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |