Metamath Proof Explorer

Theorem lplncvrlvol

Description: An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012)

Ref Expression
Hypotheses lplncvrlvol.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lplncvrlvol.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
lplncvrlvol.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
lplncvrlvol.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion lplncvrlvol ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 lplncvrlvol.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lplncvrlvol.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3 lplncvrlvol.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
4 lplncvrlvol.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
5 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑋 ∈ 𝑃 ) → 𝐾 ∈ HL )
6 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑋 ∈ 𝑃 ) → 𝑌 ∈ 𝐵 )
7 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ∈ 𝑃 )
8 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑋 ∈ 𝑃 ) → 𝑋 𝐶 𝑌 )
9 1 2 3 4 lvoli ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ 𝑉 )
10 5 6 7 8 9 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑋 ∈ 𝑃 ) → 𝑌 ∈ 𝑉 )
11 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → 𝐾 ∈ HL )
12 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝐵 )
13 11 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → 𝐾 ∈ Lat )
14 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ 𝐵 )
15 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
16 1 15 latref ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( le ‘ 𝐾 ) 𝑌 )
17 13 14 16 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ( le ‘ 𝐾 ) 𝑌 )
18 11 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑌 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ HL )
19 simplr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑌 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑌 ∈ 𝑉 )
20 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑌 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑌 ∈ ( Atoms ‘ 𝐾 ) )
21 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
22 15 21 4 lvolnleat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑉 ∧ 𝑌 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑌 ( le ‘ 𝐾 ) 𝑌 )
23 18 19 20 22 syl3anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑌 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑌 ( le ‘ 𝐾 ) 𝑌 )
24 23 ex ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑌 ∈ ( Atoms ‘ 𝐾 ) → ¬ 𝑌 ( le ‘ 𝐾 ) 𝑌 ) )
25 17 24 mt2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑌 ∈ ( Atoms ‘ 𝐾 ) )
26 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → 𝑋 𝐶 𝑌 )
27 breq1 ⊢ ( 𝑋 = ( 0. ‘ 𝐾 ) → ( 𝑋 𝐶 𝑌 ↔ ( 0. ‘ 𝐾 ) 𝐶 𝑌 ) )
28 26 27 syl5ibcom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 = ( 0. ‘ 𝐾 ) → ( 0. ‘ 𝐾 ) 𝐶 𝑌 ) )
29 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
30 1 29 2 21 isat2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∈ ( Atoms ‘ 𝐾 ) ↔ ( 0. ‘ 𝐾 ) 𝐶 𝑌 ) )
31 11 14 30 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑌 ∈ ( Atoms ‘ 𝐾 ) ↔ ( 0. ‘ 𝐾 ) 𝐶 𝑌 ) )
32 28 31 sylibrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 = ( 0. ‘ 𝐾 ) → 𝑌 ∈ ( Atoms ‘ 𝐾 ) ) )
33 32 necon3bd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ( ¬ 𝑌 ∈ ( Atoms ‘ 𝐾 ) → 𝑋 ≠ ( 0. ‘ 𝐾 ) ) )
34 25 33 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ≠ ( 0. ‘ 𝐾 ) )
35 eqid ⊢ ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
36 35 4 lvolnelln ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑌 ∈ ( LLines ‘ 𝐾 ) )
37 11 36 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑌 ∈ ( LLines ‘ 𝐾 ) )
38 11 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ HL )
39 14 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑌 ∈ 𝐵 )
40 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑋 ∈ ( Atoms ‘ 𝐾 ) )
41 simpllr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑋 𝐶 𝑌 )
42 1 2 21 35 llni ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ ( Atoms ‘ 𝐾 ) ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ ( LLines ‘ 𝐾 ) )
43 38 39 40 41 42 syl31anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑌 ∈ ( LLines ‘ 𝐾 ) )
44 37 43 mtand ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑋 ∈ ( Atoms ‘ 𝐾 ) )
45 3 4 lvolnelpln ⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑌 ∈ 𝑃 )
46 11 45 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑌 ∈ 𝑃 )
47 1 2 35 3 llncvrlpln ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 ∈ ( LLines ‘ 𝐾 ) ↔ 𝑌 ∈ 𝑃 ) )
48 47 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∈ ( LLines ‘ 𝐾 ) ↔ 𝑌 ∈ 𝑃 ) )
49 46 48 mtbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑋 ∈ ( LLines ‘ 𝐾 ) )
50 1 15 29 21 35 3 lplnle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ≠ ( 0. ‘ 𝐾 ) ∧ ¬ 𝑋 ∈ ( Atoms ‘ 𝐾 ) ∧ ¬ 𝑋 ∈ ( LLines ‘ 𝐾 ) ) ) → ∃ 𝑧 ∈ 𝑃 𝑧 ( le ‘ 𝐾 ) 𝑋 )
51 11 12 34 44 49 50 syl23anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ∃ 𝑧 ∈ 𝑃 𝑧 ( le ‘ 𝐾 ) 𝑋 )
52 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑧 ( le ‘ 𝐾 ) 𝑋 )
53 simpll1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝐾 ∈ HL )
54 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
55 53 54 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝐾 ∈ OP )
56 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑧 ∈ 𝑃 )
57 1 3 lplnbase ⊢ ( 𝑧 ∈ 𝑃 → 𝑧 ∈ 𝐵 )
58 56 57 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑧 ∈ 𝐵 )
59 simpll2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑋 ∈ 𝐵 )
60 simpll3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑌 ∈ 𝐵 )
61 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑌 ∈ 𝑉 )
62 1 15 2 cvrle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ( le ‘ 𝐾 ) 𝑌 )
63 62 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑋 ( le ‘ 𝐾 ) 𝑌 )
64 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
65 53 64 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝐾 ∈ Poset )
66 1 15 postr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑧 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 ( le ‘ 𝐾 ) 𝑌 ) → 𝑧 ( le ‘ 𝐾 ) 𝑌 ) )
67 65 58 59 60 66 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → ( ( 𝑧 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 ( le ‘ 𝐾 ) 𝑌 ) → 𝑧 ( le ‘ 𝐾 ) 𝑌 ) )
68 52 63 67 mp2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑧 ( le ‘ 𝐾 ) 𝑌 )
69 15 2 3 4 lplncvrlvol2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑧 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑧 ( le ‘ 𝐾 ) 𝑌 ) → 𝑧 𝐶 𝑌 )
70 53 56 61 68 69 syl31anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑧 𝐶 𝑌 )
71 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑋 𝐶 𝑌 )
72 1 15 2 cvrcmp2 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑧 𝐶 𝑌 ∧ 𝑋 𝐶 𝑌 ) ) → ( 𝑧 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑧 = 𝑋 ) )
73 55 58 59 60 70 71 72 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → ( 𝑧 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑧 = 𝑋 ) )
74 52 73 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑧 = 𝑋 )
75 74 56 eqeltrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ ( 𝑌 ∈ 𝑉 ∧ 𝑧 ∈ 𝑃 ∧ 𝑧 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑋 ∈ 𝑃 )
76 75 3exp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑌 ∈ 𝑉 → ( 𝑧 ∈ 𝑃 → ( 𝑧 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝑃 ) ) ) )
77 76 imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑧 ∈ 𝑃 → ( 𝑧 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝑃 ) ) )
78 77 rexlimdv ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → ( ∃ 𝑧 ∈ 𝑃 𝑧 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝑃 ) )
79 51 78 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝑃 )
80 10 79 impbida ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑉 ) )