Metamath Proof Explorer

Theorem lvolnle3at

Description: A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012)

Ref Expression
Hypotheses lvolnle3at.l ⊢ ≤ = ( le ‘ 𝐾 )
lvolnle3at.j ⊢ ∨ = ( join ‘ 𝐾 )
lvolnle3at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lvolnle3at.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
Assertion lvolnle3at ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 lvolnle3at.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lvolnle3at.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lvolnle3at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lvolnle3at.v ⊢ 𝑉 = ( LVols ‘ 𝐾 )
5 simplr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑋 ∈ 𝑉 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
8 eqid ⊢ ( LPlanes ‘ 𝐾 ) = ( LPlanes ‘ 𝐾 )
9 6 7 8 4 islvol ⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑉 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) )
10 9 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑋 ∈ 𝑉 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) )
11 5 10 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
12 11 simprd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ∃ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 )
13 oveq1 ⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑄 ) )
14 13 oveq1d ⊢ ( 𝑃 = 𝑄 → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) )
15 14 breq2d ⊢ ( 𝑃 = 𝑄 → ( 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑋 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ) )
16 15 notbid ⊢ ( 𝑃 = 𝑄 → ( ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ¬ 𝑋 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ) )
17 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝐾 ∈ HL )
18 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑦 ∈ ( LPlanes ‘ 𝐾 ) )
19 simp21 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑃 ∈ 𝐴 )
20 simp22 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑄 ∈ 𝐴 )
21 1 2 3 8 lplnnle2at ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) )
22 17 18 19 20 21 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) )
23 6 8 lplnbase ⊢ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
24 18 23 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) )
25 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑋 ∈ 𝑉 )
26 6 4 lvolbase ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ ( Base ‘ 𝐾 ) )
27 25 26 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑋 ∈ ( Base ‘ 𝐾 ) )
28 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 )
29 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
30 6 29 7 cvrlt ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) → 𝑦 ( lt ‘ 𝐾 ) 𝑋 )
31 17 24 27 28 30 syl31anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑦 ( lt ‘ 𝐾 ) 𝑋 )
32 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
33 17 32 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝐾 ∈ Poset )
34 6 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
35 17 19 20 34 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
36 6 1 29 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
37 33 24 27 35 36 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
38 31 37 mpand ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑋 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑦 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
39 1 29 pltle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑦 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) → 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) )
40 17 18 35 39 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑦 ( lt ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) → 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) )
41 38 40 syld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑋 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑦 ≤ ( 𝑃 ∨ 𝑄 ) ) )
42 22 41 mtod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑋 ≤ ( 𝑃 ∨ 𝑄 ) )
43 42 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑋 ≤ ( 𝑃 ∨ 𝑄 ) )
44 simprr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
45 17 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝐾 ∈ Lat )
46 simp23 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑅 ∈ 𝐴 )
47 6 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
48 46 47 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
49 6 1 2 latleeqj2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) ) )
50 45 48 35 49 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) ) )
51 50 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) ) )
52 44 51 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ 𝑄 ) )
53 52 breq2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑋 ≤ ( 𝑃 ∨ 𝑄 ) ) )
54 43 53 mtbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
55 54 anassrs ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
56 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
57 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑦 ∈ ( LPlanes ‘ 𝐾 ) )
58 simpl2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
59 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
60 1 2 3 8 lplni2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) )
61 56 58 59 60 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) )
62 29 8 lplnnlt ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( LPlanes ‘ 𝐾 ) ) → ¬ 𝑦 ( lt ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
63 56 57 61 62 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑦 ( lt ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
64 6 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
65 45 35 48 64 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
66 6 1 29 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑦 ( lt ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
67 33 24 27 65 66 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → 𝑦 ( lt ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
68 31 67 mpand ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) → 𝑦 ( lt ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
69 68 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) → 𝑦 ( lt ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
70 63 69 mtod ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
71 70 anassrs ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
72 55 71 pm2.61dan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ∧ 𝑃 ≠ 𝑄 ) → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
73 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
74 73 2 3 8 lplnnle2at ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ 𝑦 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
75 17 18 20 46 74 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑦 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) )
76 6 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
77 17 20 46 76 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
78 6 1 29 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
79 33 24 27 77 78 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( ( 𝑦 ( lt ‘ 𝐾 ) 𝑋 ∧ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
80 31 79 mpand ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) → 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
81 73 29 pltle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
82 17 18 77 81 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑦 ( lt ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
83 80 82 syld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑄 ∨ 𝑅 ) ) )
84 75 83 mtod ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) )
85 2 3 hlatjidm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
86 17 20 85 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 )
87 86 oveq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) )
88 87 breq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ( 𝑋 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑋 ≤ ( 𝑄 ∨ 𝑅 ) ) )
89 84 88 mtbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑋 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) )
90 16 72 89 pm2.61ne ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )
91 90 3expia ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) ∧ 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 ) → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
92 91 expd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑦 ∈ ( LPlanes ‘ 𝐾 ) → ( 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) )
93 92 rexlimdv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ∃ 𝑦 ∈ ( LPlanes ‘ 𝐾 ) 𝑦 ( ⋖ ‘ 𝐾 ) 𝑋 → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) )
94 12 93 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ¬ 𝑋 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) )