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