This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lhp2at0nle

Description: Inequality for 2 different atoms (or an atom and zero) under co-atom W . (Contributed by NM, 28-Jul-2013)

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

Proof

Step Hyp Ref Expression
1 lhp2at0nle.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhp2at0nle.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lhp2at0nle.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 lhp2at0nle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 lhp2at0nle.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 simpl1 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑈 ∈ 𝐴 ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) )
7 simpr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑈 ∈ 𝐴 ) → 𝑈 ∈ 𝐴 )
8 simpl2r ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑈 ∈ 𝐴 ) → 𝑈 ≤ 𝑊 )
9 simpl3 ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑈 ∈ 𝐴 ) → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
10 1 2 4 5 lhp2atnle ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) )
11 6 7 8 9 10 syl121anc ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑈 ∈ 𝐴 ) → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) )
12 simp3r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ≤ 𝑊 )
13 simp12r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ¬ 𝑃 ≤ 𝑊 )
14 nbrne2 ⊢ ( ( 𝑉 ≤ 𝑊 ∧ ¬ 𝑃 ≤ 𝑊 ) → 𝑉 ≠ 𝑃 )
15 12 13 14 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ≠ 𝑃 )
16 15 neneqd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ¬ 𝑉 = 𝑃 )
17 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
18 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
19 17 18 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ AtLat )
20 simp3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑉 ∈ 𝐴 )
21 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
22 1 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑉 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑉 ≤ 𝑃 ↔ 𝑉 = 𝑃 ) )
23 19 20 21 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑉 ≤ 𝑃 ↔ 𝑉 = 𝑃 ) )
24 16 23 mtbird ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ¬ 𝑉 ≤ 𝑃 )
25 24 adantr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑈 = 0 ) → ¬ 𝑉 ≤ 𝑃 )
26 oveq2 ⊢ ( 𝑈 = 0 → ( 𝑃 ∨ 𝑈 ) = ( 𝑃 ∨ 0 ) )
27 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
28 17 27 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝐾 ∈ OL )
29 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
30 29 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
31 21 30 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
32 29 2 3 olj01 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 0 ) = 𝑃 )
33 28 31 32 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑃 ∨ 0 ) = 𝑃 )
34 26 33 sylan9eqr ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑈 = 0 ) → ( 𝑃 ∨ 𝑈 ) = 𝑃 )
35 34 breq2d ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑈 = 0 ) → ( 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) ↔ 𝑉 ≤ 𝑃 ) )
36 25 35 mtbird ⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) ∧ 𝑈 = 0 ) → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) )
37 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) )
38 11 36 37 mpjaodan ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ 𝑈 ≠ 𝑉 ) ∧ ( ( 𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) )