Metamath Proof Explorer

Theorem atle

Description: Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012)

Ref Expression
Hypotheses atle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
atle.l ⊢ ≤ = ( le ‘ 𝐾 )
atle.z ⊢ 0 = ( 0. ‘ 𝐾 )
atle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atle ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑋 )

Proof

Step Hyp Ref Expression
1 atle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 atle.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 atle.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝐾 ∈ HL )
6 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
7 6 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝐾 ∈ OP )
8 1 3 op0cl ⊢ ( 𝐾 ∈ OP → 0 ∈ 𝐵 )
9 7 8 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 0 ∈ 𝐵 )
10 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐵 )
11 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
12 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
13 1 12 3 opltn0 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( lt ‘ 𝐾 ) 𝑋 ↔ 𝑋 ≠ 0 ) )
14 7 10 13 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 0 ( lt ‘ 𝐾 ) 𝑋 ↔ 𝑋 ≠ 0 ) )
15 11 14 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 0 ( lt ‘ 𝐾 ) 𝑋 )
16 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
17 1 2 12 16 4 hlrelat ⊢ ( ( ( 𝐾 ∈ HL ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 0 ( lt ‘ 𝐾 ) 𝑋 ) → ∃ 𝑝 ∈ 𝐴 ( 0 ( lt ‘ 𝐾 ) ( 0 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 0 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) )
18 5 9 10 15 17 syl31anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃ 𝑝 ∈ 𝐴 ( 0 ( lt ‘ 𝐾 ) ( 0 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 0 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) )
19 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ HL )
20 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
21 19 20 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑝 ∈ 𝐴 ) → 𝐾 ∈ OL )
22 1 4 atbase ⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵 )
23 22 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ 𝐵 )
24 1 16 3 olj02 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑝 ∈ 𝐵 ) → ( 0 ( join ‘ 𝐾 ) 𝑝 ) = 𝑝 )
25 21 23 24 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑝 ∈ 𝐴 ) → ( 0 ( join ‘ 𝐾 ) 𝑝 ) = 𝑝 )
26 25 breq1d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 0 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ↔ 𝑝 ≤ 𝑋 ) )
27 26 biimpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 0 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 → 𝑝 ≤ 𝑋 ) )
28 27 adantld ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 0 ( lt ‘ 𝐾 ) ( 0 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 0 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → 𝑝 ≤ 𝑋 ) )
29 28 reximdva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( ∃ 𝑝 ∈ 𝐴 ( 0 ( lt ‘ 𝐾 ) ( 0 ( join ‘ 𝐾 ) 𝑝 ) ∧ ( 0 ( join ‘ 𝐾 ) 𝑝 ) ≤ 𝑋 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑋 ) )
30 18 29 mpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑋 )