Step | Hyp | Ref
| Expression |
1 | | djhval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | djhval.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
3 | | djhval.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑈) |
4 | | djhval.o |
. . . . 5
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
5 | | djhval.j |
. . . . 5
⊢ ∨ =
((joinH‘𝐾)‘𝑊) |
6 | 1, 2, 3, 4, 5 | djhfval 36686 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
7 | 6 | adantr 481 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
8 | 7 | oveqd 6667 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) = (𝑋(𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))𝑌)) |
9 | | fvex 6201 |
. . . . . . 7
⊢
(Base‘𝑈)
∈ V |
10 | 3, 9 | eqeltri 2697 |
. . . . . 6
⊢ 𝑉 ∈ V |
11 | 10 | elpw2 4828 |
. . . . 5
⊢ (𝑋 ∈ 𝒫 𝑉 ↔ 𝑋 ⊆ 𝑉) |
12 | 11 | biimpri 218 |
. . . 4
⊢ (𝑋 ⊆ 𝑉 → 𝑋 ∈ 𝒫 𝑉) |
13 | 12 | ad2antrl 764 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → 𝑋 ∈ 𝒫 𝑉) |
14 | 10 | elpw2 4828 |
. . . . 5
⊢ (𝑌 ∈ 𝒫 𝑉 ↔ 𝑌 ⊆ 𝑉) |
15 | 14 | biimpri 218 |
. . . 4
⊢ (𝑌 ⊆ 𝑉 → 𝑌 ∈ 𝒫 𝑉) |
16 | 15 | ad2antll 765 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → 𝑌 ∈ 𝒫 𝑉) |
17 | | fvexd 6203 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌))) ∈
V) |
18 | | fveq2 6191 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑋)) |
19 | 18 | ineq1d 3813 |
. . . . 5
⊢ (𝑥 = 𝑋 → (( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑦))) |
20 | 19 | fveq2d 6195 |
. . . 4
⊢ (𝑥 = 𝑋 → ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))) = ( ⊥
‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑦)))) |
21 | | fveq2 6191 |
. . . . . 6
⊢ (𝑦 = 𝑌 → ( ⊥ ‘𝑦) = ( ⊥ ‘𝑌)) |
22 | 21 | ineq2d 3814 |
. . . . 5
⊢ (𝑦 = 𝑌 → (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑦)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) |
23 | 22 | fveq2d 6195 |
. . . 4
⊢ (𝑦 = 𝑌 → ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑦))) = ( ⊥
‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌)))) |
24 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) |
25 | 20, 23, 24 | ovmpt2g 6795 |
. . 3
⊢ ((𝑋 ∈ 𝒫 𝑉 ∧ 𝑌 ∈ 𝒫 𝑉 ∧ ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌))) ∈ V)
→ (𝑋(𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))𝑌) = ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌)))) |
26 | 13, 16, 17, 25 | syl3anc 1326 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋(𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))𝑌) = ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌)))) |
27 | 8, 26 | eqtrd 2656 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) = ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌)))) |