| Step | Hyp | Ref
| Expression |
| 1 | | djhval.j |
. . 3
⊢ ∨ =
((joinH‘𝐾)‘𝑊) |
| 2 | | djhval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 3 | 2 | djhffval 41398 |
. . . 4
⊢ (𝐾 ∈ 𝑋 → (joinH‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))) |
| 4 | 3 | fveq1d 6908 |
. . 3
⊢ (𝐾 ∈ 𝑋 → ((joinH‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))‘𝑊)) |
| 5 | 1, 4 | eqtrid 2789 |
. 2
⊢ (𝐾 ∈ 𝑋 → ∨ = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))‘𝑊)) |
| 6 | | 2fveq3 6911 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘((DVecH‘𝐾)‘𝑤)) = (Base‘((DVecH‘𝐾)‘𝑊))) |
| 7 | | djhval.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
| 8 | | djhval.u |
. . . . . . . 8
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| 9 | 8 | fveq2i 6909 |
. . . . . . 7
⊢
(Base‘𝑈) =
(Base‘((DVecH‘𝐾)‘𝑊)) |
| 10 | 7, 9 | eqtri 2765 |
. . . . . 6
⊢ 𝑉 =
(Base‘((DVecH‘𝐾)‘𝑊)) |
| 11 | 6, 10 | eqtr4di 2795 |
. . . . 5
⊢ (𝑤 = 𝑊 → (Base‘((DVecH‘𝐾)‘𝑤)) = 𝑉) |
| 12 | 11 | pweqd 4617 |
. . . 4
⊢ (𝑤 = 𝑊 → 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) = 𝒫 𝑉) |
| 13 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((ocH‘𝐾)‘𝑤) = ((ocH‘𝐾)‘𝑊)) |
| 14 | | djhval.o |
. . . . . 6
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
| 15 | 13, 14 | eqtr4di 2795 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((ocH‘𝐾)‘𝑤) = ⊥ ) |
| 16 | 15 | fveq1d 6908 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((ocH‘𝐾)‘𝑤)‘𝑥) = ( ⊥ ‘𝑥)) |
| 17 | 15 | fveq1d 6908 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((ocH‘𝐾)‘𝑤)‘𝑦) = ( ⊥ ‘𝑦)) |
| 18 | 16, 17 | ineq12d 4221 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)) = (( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦))) |
| 19 | 15, 18 | fveq12d 6913 |
. . . 4
⊢ (𝑤 = 𝑊 → (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦))) = ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) |
| 20 | 12, 12, 19 | mpoeq123dv 7508 |
. . 3
⊢ (𝑤 = 𝑊 → (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))) = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
| 21 | | eqid 2737 |
. . 3
⊢ (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦))))) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦))))) |
| 22 | 7 | fvexi 6920 |
. . . . 5
⊢ 𝑉 ∈ V |
| 23 | 22 | pwex 5380 |
. . . 4
⊢ 𝒫
𝑉 ∈ V |
| 24 | 23, 23 | mpoex 8104 |
. . 3
⊢ (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) ∈
V |
| 25 | 20, 21, 24 | fvmpt 7016 |
. 2
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)), 𝑦 ∈ 𝒫
(Base‘((DVecH‘𝐾)‘𝑤)) ↦ (((ocH‘𝐾)‘𝑤)‘((((ocH‘𝐾)‘𝑤)‘𝑥) ∩ (((ocH‘𝐾)‘𝑤)‘𝑦)))))‘𝑊) = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
| 26 | 5, 25 | sylan9eq 2797 |
1
⊢ ((𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |