Theorem exatleN

Description: A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in Crawley p. 112. (Contributed by NM, 28-Apr-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	atomle.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	atomle.l	⊢ ≤ = ( le ‘ 𝐾 )
	atomle.j	⊢ ∨ = ( join ‘ 𝐾 )
	atomle.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	exatleN	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≤ 𝑋 ↔ 𝑅 = 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		atomle.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		atomle.l	⊢ ≤ = ( le ‘ 𝐾 )
3		atomle.j	⊢ ∨ = ( join ‘ 𝐾 )
4		atomle.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		simpl32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ) → ¬ 𝑄 ≤ 𝑋 )
6		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝐾 ∈ HL )
7	6	hllatd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝐾 ∈ Lat )
8		simp122	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑄 ∈ 𝐴 )
9	1 4	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
10	8 9	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑄 ∈ 𝐵 )
11		simp121	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑃 ∈ 𝐴 )
12	1 4	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
13	11 12	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑃 ∈ 𝐵 )
14		simp123	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ∈ 𝐴 )
15	1 4	atbase	⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵 )
16	14 15	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ∈ 𝐵 )
17	1 3	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑅 ) ∈ 𝐵 )
18	7 13 16 17	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → ( 𝑃 ∨ 𝑅 ) ∈ 𝐵 )
19		simp11r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
20	14 8 11	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → ( 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) )
21		simp2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ≠ 𝑃 )
22	6 20 21	3jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ≠ 𝑃 ) )
23		simp133	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) )
24	2 3 4	hlatexch1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑅 ≠ 𝑃 ) → ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ) )
25	22 23 24	sylc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) )
26		simp131	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑃 ≤ 𝑋 )
27		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑅 ≤ 𝑋 )
28	1 2 3	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑅 ≤ 𝑋 ) ↔ ( 𝑃 ∨ 𝑅 ) ≤ 𝑋 ) )
29	7 13 16 19 28	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → ( ( 𝑃 ≤ 𝑋 ∧ 𝑅 ≤ 𝑋 ) ↔ ( 𝑃 ∨ 𝑅 ) ≤ 𝑋 ) )
30	26 27 29	mpbi2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → ( 𝑃 ∨ 𝑅 ) ≤ 𝑋 )
31	1 2 7 10 18 19 25 30	lattrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋 ) → 𝑄 ≤ 𝑋 )
32	31	3expia	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ) → ( 𝑅 ≤ 𝑋 → 𝑄 ≤ 𝑋 ) )
33	5 32	mtod	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ 𝑅 ≠ 𝑃 ) → ¬ 𝑅 ≤ 𝑋 )
34	33	ex	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≠ 𝑃 → ¬ 𝑅 ≤ 𝑋 ) )
35	34	necon4ad	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≤ 𝑋 → 𝑅 = 𝑃 ) )
36		simp31	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → 𝑃 ≤ 𝑋 )
37		breq1	⊢ ( 𝑅 = 𝑃 → ( 𝑅 ≤ 𝑋 ↔ 𝑃 ≤ 𝑋 ) )
38	36 37	syl5ibrcom	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 = 𝑃 → 𝑅 ≤ 𝑋 ) )
39	35 38	impbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( 𝑅 ≤ 𝑋 ↔ 𝑅 = 𝑃 ) )