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 ) ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) ) → ¬ 𝑉 ≤ ( 𝑃 ∨ 𝑈 ) )