Metamath Proof Explorer


Theorem 0ltat

Description: An atom is greater than zero. (Contributed by NM, 4-Jul-2012)

Ref Expression
Hypotheses 0ltat.z 0 = ( 0. ‘ 𝐾 )
0ltat.s < = ( lt ‘ 𝐾 )
0ltat.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 0ltat ( ( 𝐾 ∈ OP ∧ 𝑃𝐴 ) → 0 < 𝑃 )

Proof

Step Hyp Ref Expression
1 0ltat.z 0 = ( 0. ‘ 𝐾 )
2 0ltat.s < = ( lt ‘ 𝐾 )
3 0ltat.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simpl ( ( 𝐾 ∈ OP ∧ 𝑃𝐴 ) → 𝐾 ∈ OP )
5 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 5 1 op0cl ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
7 6 adantr ( ( 𝐾 ∈ OP ∧ 𝑃𝐴 ) → 0 ∈ ( Base ‘ 𝐾 ) )
8 5 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
9 8 adantl ( ( 𝐾 ∈ OP ∧ 𝑃𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
10 eqid ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
11 1 10 3 atcvr0 ( ( 𝐾 ∈ OP ∧ 𝑃𝐴 ) → 0 ( ⋖ ‘ 𝐾 ) 𝑃 )
12 5 2 10 cvrlt ( ( ( 𝐾 ∈ OP ∧ 0 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ∧ 0 ( ⋖ ‘ 𝐾 ) 𝑃 ) → 0 < 𝑃 )
13 4 7 9 11 12 syl31anc ( ( 𝐾 ∈ OP ∧ 𝑃𝐴 ) → 0 < 𝑃 )