Metamath Proof Explorer

Theorem lhp2atnle

Description: Inequality for 2 different atoms under co-atom W . (Contributed by NM, 17-Jun-2013)

Ref Expression
Hypotheses lhp2atnle.l ⊢ ≤ = ( le ‘ 𝐾 )
lhp2atnle.j ⊢ ∨ = ( join ‘ 𝐾 )
lhp2atnle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhp2atnle.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhp2atnle ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 lhp2atnle.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhp2atnle.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lhp2atnle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lhp2atnle.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
6 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
7 5 6 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ AtLat )
8 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ∈ 𝐴 )
9 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
10 9 3 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑉 ∈ 𝐴 ) → 𝑉 ≠ ( 0. ‘ 𝐾 ) )
11 7 8 10 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ≠ ( 0. ‘ 𝐾 ) )
12 5 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 3 atbase ⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
15 8 14 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ∈ ( Base ‘ 𝐾 ) )
16 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
17 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑈 ∈ 𝐴 )
18 13 2 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
19 5 16 17 18 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
20 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
21 13 1 20 latleeqm2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) ↔ ( ( 𝑃 ∨ 𝑈 ) ( meet ‘ 𝐾 ) 𝑉 ) = 𝑉 ) )
22 12 15 19 21 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) ↔ ( ( 𝑃 ∨ 𝑈 ) ( meet ‘ 𝐾 ) 𝑉 ) = 𝑉 ) )
23 1 2 20 9 3 4 lhp2at0 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑈 ) ( meet ‘ 𝐾 ) 𝑉 ) = ( 0. ‘ 𝐾 ) )
24 eqeq1 ⊢ ( ( ( 𝑃 ∨ 𝑈 ) ( meet ‘ 𝐾 ) 𝑉 ) = 𝑉 → ( ( ( 𝑃 ∨ 𝑈 ) ( meet ‘ 𝐾 ) 𝑉 ) = ( 0. ‘ 𝐾 ) ↔ 𝑉 = ( 0. ‘ 𝐾 ) ) )
25 23 24 syl5ibcom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( ( ( 𝑃 ∨ 𝑈 ) ( meet ‘ 𝐾 ) 𝑉 ) = 𝑉 → 𝑉 = ( 0. ‘ 𝐾 ) ) )
26 22 25 sylbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) → 𝑉 = ( 0. ‘ 𝐾 ) ) )
27 26 necon3ad ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑉 ≠ ( 0. ‘ 𝐾 ) → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) ) )
28 11 27 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) )