Metamath Proof Explorer


Theorem dihord4

Description: The isomorphism H for a lattice K is order-preserving in the region not under co-atom W . TODO: reformat ( q e. A /\ -. q .<_ W ) to eliminate adant*. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihord3.b 𝐵 = ( Base ‘ 𝐾 )
dihord3.l = ( le ‘ 𝐾 )
dihord3.h 𝐻 = ( LHyp ‘ 𝐾 )
dihord3.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihord4 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ ( 𝑌𝐵 ∧ ¬ 𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )

Proof

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 ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ ( 𝑌𝐵 ∧ ¬ 𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )