Step |
Hyp |
Ref |
Expression |
1 |
|
dia1eldm.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
dia1eldm.i |
⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
4 |
3 1
|
lhpbase |
⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) ) |
6 |
|
hllat |
⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat ) |
7 |
|
eqid |
⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) |
8 |
3 7
|
latref |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → 𝑊 ( le ‘ 𝐾 ) 𝑊 ) |
9 |
6 4 8
|
syl2an |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ( le ‘ 𝐾 ) 𝑊 ) |
10 |
3 7 1 2
|
diaeldm |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑊 ∈ dom 𝐼 ↔ ( 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ( le ‘ 𝐾 ) 𝑊 ) ) ) |
11 |
5 9 10
|
mpbir2and |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ dom 𝐼 ) |