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

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 < 𝑃 )