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 )