Step |
Hyp |
Ref |
Expression |
1 |
|
dihord3.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
dihord3.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
dihord3.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
4 |
|
dihord3.i |
⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
6 |
|
eqid |
⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 ) |
7 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
8 |
1 2 5 6 7 3
|
lhpmcvr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) |
9 |
8
|
3adant3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) |
10 |
1 2 5 6 7 3
|
lhpmcvr2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) |
11 |
10
|
3adant2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) |
12 |
|
reeanv |
⊢ ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ↔ ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) |
13 |
9 11 12
|
sylanbrc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) |
14 |
|
simp11 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
15 |
|
simp12 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ) |
16 |
|
simp2l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) |
17 |
|
simp3ll |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ¬ 𝑞 ≤ 𝑊 ) |
18 |
16 17
|
jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) ) |
19 |
|
simp3lr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) |
20 |
|
eqid |
⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) |
21 |
|
eqid |
⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) |
22 |
|
eqid |
⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
23 |
|
eqid |
⊢ ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) |
24 |
1 2 5 6 7 3 4 20 21 22 23
|
dihvalcq |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
25 |
14 15 18 19 24
|
syl112anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
26 |
|
simp13 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) |
27 |
|
simp2r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) |
28 |
|
simp3rl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ¬ 𝑟 ≤ 𝑊 ) |
29 |
27 28
|
jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ) |
30 |
|
simp3rr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) |
31 |
1 2 5 6 7 3 4 20 21 22 23
|
dihvalcq |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ∧ ( ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) → ( 𝐼 ‘ 𝑌 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
32 |
14 26 29 30 31
|
syl112anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( 𝐼 ‘ 𝑌 ) = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
33 |
25 32
|
sseq12d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) |
34 |
|
simpl11 |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
35 |
|
simpl2l |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) |
36 |
17
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ¬ 𝑞 ≤ 𝑊 ) |
37 |
35 36
|
jca |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) ) |
38 |
|
simpl2r |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) |
39 |
28
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ¬ 𝑟 ≤ 𝑊 ) |
40 |
38 39
|
jca |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ) |
41 |
|
simp12l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → 𝑋 ∈ 𝐵 ) |
42 |
41
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑋 ∈ 𝐵 ) |
43 |
|
simp13l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → 𝑌 ∈ 𝐵 ) |
44 |
43
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑌 ∈ 𝐵 ) |
45 |
19
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) |
46 |
30
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) |
47 |
|
simpr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
48 |
1 2 5 6 7 3 20 21 22 23
|
dihord2 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) → 𝑋 ≤ 𝑌 ) |
49 |
34 37 40 42 44 45 46 47 48
|
syl323anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) → 𝑋 ≤ 𝑌 ) |
50 |
|
simpl11 |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
51 |
|
simpl2l |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) |
52 |
17
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ¬ 𝑞 ≤ 𝑊 ) |
53 |
51 52
|
jca |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) ) |
54 |
|
simpl2r |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) |
55 |
28
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ¬ 𝑟 ≤ 𝑊 ) |
56 |
54 55
|
jca |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ) |
57 |
41
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ 𝐵 ) |
58 |
43
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ 𝐵 ) |
59 |
19
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) |
60 |
30
|
adantr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) |
61 |
|
simpr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 ) |
62 |
1 2 5 6 7 3 20 21 22 23
|
dihord1 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑟 ≤ 𝑊 ) ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ∧ 𝑋 ≤ 𝑌 ) ) → ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
63 |
50 53 56 57 58 59 60 61 62
|
syl323anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) ∧ 𝑋 ≤ 𝑌 ) → ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) |
64 |
49 63
|
impbida |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ⊆ ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ↔ 𝑋 ≤ 𝑌 ) ) |
65 |
33 64
|
bitrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) ) |
66 |
65
|
3exp |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) ) ) ) |
67 |
66
|
rexlimdvv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ≤ 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑋 ) ∧ ( ¬ 𝑟 ≤ 𝑊 ∧ ( 𝑟 ( join ‘ 𝐾 ) ( 𝑌 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑌 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) ) ) |
68 |
13 67
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ ( 𝑌 ∈ 𝐵 ∧ ¬ 𝑌 ≤ 𝑊 ) ) → ( ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝐼 ‘ 𝑌 ) ↔ 𝑋 ≤ 𝑌 ) ) |