Step | Hyp | Ref
| Expression |
1 | | djaval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
2 | | djaval.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
3 | | djaval.i |
. . . . 5
⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) |
4 | | djaval.n |
. . . . 5
⊢ ⊥ =
((ocA‘𝐾)‘𝑊) |
5 | | djaval.j |
. . . . 5
⊢ 𝐽 = ((vA‘𝐾)‘𝑊) |
6 | 1, 2, 3, 4, 5 | djafvalN 38760 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐽 = (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
7 | 6 | adantr 484 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → 𝐽 = (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))) |
8 | 7 | oveqd 7181 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → (𝑋𝐽𝑌) = (𝑋(𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))𝑌)) |
9 | 2 | fvexi 6682 |
. . . . . 6
⊢ 𝑇 ∈ V |
10 | 9 | elpw2 5210 |
. . . . 5
⊢ (𝑋 ∈ 𝒫 𝑇 ↔ 𝑋 ⊆ 𝑇) |
11 | 10 | biimpri 231 |
. . . 4
⊢ (𝑋 ⊆ 𝑇 → 𝑋 ∈ 𝒫 𝑇) |
12 | 11 | ad2antrl 728 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → 𝑋 ∈ 𝒫 𝑇) |
13 | 9 | elpw2 5210 |
. . . . 5
⊢ (𝑌 ∈ 𝒫 𝑇 ↔ 𝑌 ⊆ 𝑇) |
14 | 13 | biimpri 231 |
. . . 4
⊢ (𝑌 ⊆ 𝑇 → 𝑌 ∈ 𝒫 𝑇) |
15 | 14 | ad2antll 729 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → 𝑌 ∈ 𝒫 𝑇) |
16 | | fvexd 6683 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌))) ∈
V) |
17 | | fveq2 6668 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑋)) |
18 | 17 | ineq1d 4100 |
. . . . 5
⊢ (𝑥 = 𝑋 → (( ⊥ ‘𝑥) ∩ ( ⊥ ‘𝑦)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑦))) |
19 | 18 | fveq2d 6672 |
. . . 4
⊢ (𝑥 = 𝑋 → ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))) = ( ⊥
‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑦)))) |
20 | | fveq2 6668 |
. . . . . 6
⊢ (𝑦 = 𝑌 → ( ⊥ ‘𝑦) = ( ⊥ ‘𝑌)) |
21 | 20 | ineq2d 4101 |
. . . . 5
⊢ (𝑦 = 𝑌 → (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑦)) = (( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) |
22 | 21 | fveq2d 6672 |
. . . 4
⊢ (𝑦 = 𝑌 → ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑦))) = ( ⊥
‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌)))) |
23 | | eqid 2738 |
. . . 4
⊢ (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) = (𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦)))) |
24 | 19, 22, 23 | ovmpog 7318 |
. . 3
⊢ ((𝑋 ∈ 𝒫 𝑇 ∧ 𝑌 ∈ 𝒫 𝑇 ∧ ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌))) ∈ V)
→ (𝑋(𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))𝑌) = ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌)))) |
25 | 12, 15, 16, 24 | syl3anc 1372 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → (𝑋(𝑥 ∈ 𝒫 𝑇, 𝑦 ∈ 𝒫 𝑇 ↦ ( ⊥ ‘(( ⊥
‘𝑥) ∩ ( ⊥
‘𝑦))))𝑌) = ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌)))) |
26 | 8, 25 | eqtrd 2773 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇)) → (𝑋𝐽𝑌) = ( ⊥ ‘(( ⊥
‘𝑋) ∩ ( ⊥
‘𝑌)))) |