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

Metamath Proof Explorer

Theorem atlen0

Description: A lattice element is nonzero if an atom is under it. (Contributed by NM, 26-May-2012)

Ref Expression
Hypotheses atlen0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
atlen0.l ⊢ ≤ = ( le ‘ 𝐾 )
atlen0.z ⊢ 0 = ( 0. ‘ 𝐾 )
atlen0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atlen0 ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑋 ≠ 0 )

Proof

Step Hyp Ref Expression
1 atlen0.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atlen0.l ⊢ ≤ = ( le ‘ 𝐾 )
3 atlen0.z ⊢ 0 = ( 0. ‘ 𝐾 )
4 atlen0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simpl1 ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝐾 ∈ AtLat )
6 1 3 atl0cl ⊢ ( 𝐾 ∈ AtLat → 0 ∈ 𝐵 )
7 5 6 syl ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 0 ∈ 𝐵 )
8 simpl2 ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑋 ∈ 𝐵 )
9 5 7 8 3jca ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → ( 𝐾 ∈ AtLat ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
10 simpl3 ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 ∈ 𝐴 )
11 1 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
12 10 11 syl ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 ∈ 𝐵 )
13 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
14 3 13 4 atcvr0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 0 ( ⋖ ‘ 𝐾 ) 𝑃 )
15 5 10 14 syl2anc ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 0 ( ⋖ ‘ 𝐾 ) 𝑃 )
16 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
17 1 16 13 cvrlt ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 0 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) ∧ 0 ( ⋖ ‘ 𝐾 ) 𝑃 ) → 0 ( lt ‘ 𝐾 ) 𝑃 )
18 5 7 12 15 17 syl31anc ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 0 ( lt ‘ 𝐾 ) 𝑃 )
19 simpr ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑃 ≤ 𝑋 )
20 atlpos ⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ Poset )
21 5 20 syl ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝐾 ∈ Poset )
22 1 2 16 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 0 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 0 ( lt ‘ 𝐾 ) 𝑃 ∧ 𝑃 ≤ 𝑋 ) → 0 ( lt ‘ 𝐾 ) 𝑋 ) )
23 21 7 12 8 22 syl13anc ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → ( ( 0 ( lt ‘ 𝐾 ) 𝑃 ∧ 𝑃 ≤ 𝑋 ) → 0 ( lt ‘ 𝐾 ) 𝑋 ) )
24 18 19 23 mp2and ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 0 ( lt ‘ 𝐾 ) 𝑋 )
25 16 pltne ⊢ ( ( 𝐾 ∈ AtLat ∧ 0 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 0 ( lt ‘ 𝐾 ) 𝑋 → 0 ≠ 𝑋 ) )
26 9 24 25 sylc ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 0 ≠ 𝑋 )
27 26 necomd ⊢ ( ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑃 ≤ 𝑋 ) → 𝑋 ≠ 0 )