Step |
Hyp |
Ref |
Expression |
1 |
|
djacl.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
djacl.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
djacl.i |
⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
djacl.j |
⊢ 𝐽 = ( ( vA ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
eqid |
⊢ ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) |
6 |
1 2 3 5 4
|
djavalN |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( 𝑋 𝐽 𝑌 ) = ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) ) |
7 |
|
inss1 |
⊢ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ⊆ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) |
8 |
1 2 3 5
|
docaclN |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑇 ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ ran 𝐼 ) |
9 |
8
|
adantrr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ ran 𝐼 ) |
10 |
1 2 3
|
diaelrnN |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∈ ran 𝐼 ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ⊆ 𝑇 ) |
11 |
9 10
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ⊆ 𝑇 ) |
12 |
7 11
|
sstrid |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ⊆ 𝑇 ) |
13 |
1 2 3 5
|
docaclN |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ⊆ 𝑇 ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) ∈ ran 𝐼 ) |
14 |
12 13
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) ∩ ( ( ( ocA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑌 ) ) ) ∈ ran 𝐼 ) |
15 |
6 14
|
eqeltrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑇 ∧ 𝑌 ⊆ 𝑇 ) ) → ( 𝑋 𝐽 𝑌 ) ∈ ran 𝐼 ) |