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 35704 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
7 | 6 | adantr 480 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → ∨ = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
8 | 7 | oveqd 6566 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) = (𝑋(𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))𝑌)) |
9 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝑈)
∈ V |
10 | 3, 9 | eqeltri 2684 |
. . . . . 6
⊢ 𝑉 ∈ V |
11 | 10 | elpw2 4755 |
. . . . 5
⊢ (𝑋 ∈ 𝒫 𝑉 ↔ 𝑋 ⊆ 𝑉) |
12 | 11 | biimpri 217 |
. . . 4
⊢ (𝑋 ⊆ 𝑉 → 𝑋 ∈ 𝒫 𝑉) |
13 | 12 | ad2antrl 760 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → 𝑋 ∈ 𝒫 𝑉) |
14 | 10 | elpw2 4755 |
. . . . 5
⊢ (𝑌 ∈ 𝒫 𝑉 ↔ 𝑌 ⊆ 𝑉) |
15 | 14 | biimpri 217 |
. . . 4
⊢ (𝑌 ⊆ 𝑉 → 𝑌 ∈ 𝒫 𝑉) |
16 | 15 | ad2antll 761 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → 𝑌 ∈ 𝒫 𝑉) |
17 | | fvex 6113 |
. . . 4
⊢ ( ⊥
‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) ∈ V |
18 | 17 | a1i 11 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌))) ∈
V) |
19 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑋)) |
20 | 19 | ineq1d 3775 |
. . . . 5
⊢ (𝑥 = 𝑋 → (( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑦))) |
21 | 20 | fveq2d 6107 |
. . . 4
⊢ (𝑥 = 𝑋 → ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))) = ( ⊥
‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑦)))) |
22 | | fveq2 6103 |
. . . . . 6
⊢ (𝑦 = 𝑌 → ( ⊥ ‘𝑦) = ( ⊥ ‘𝑌)) |
23 | 22 | ineq2d 3776 |
. . . . 5
⊢ (𝑦 = 𝑌 → (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑦)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) |
24 | 23 | fveq2d 6107 |
. . . 4
⊢ (𝑦 = 𝑌 → ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑦))) = ( ⊥
‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌)))) |
25 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) = (𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) |
26 | 21, 24, 25 | ovmpt2g 6693 |
. . 3
⊢ ((𝑋 ∈ 𝒫 𝑉 ∧ 𝑌 ∈ 𝒫 𝑉 ∧ ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌))) ∈ V)
→ (𝑋(𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))𝑌) = ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌)))) |
27 | 13, 16, 18, 26 | syl3anc 1318 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋(𝑥 ∈ 𝒫 𝑉, 𝑦 ∈ 𝒫 𝑉 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))𝑌) = ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌)))) |
28 | 8, 27 | eqtrd 2644 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉)) → (𝑋 ∨ 𝑌) = ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌)))) |