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

Metamath Proof Explorer

Theorem lplnn0N

Description: A lattice plane is nonzero. (Contributed by NM, 15-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses lplnn0.z ⊢ 0 = ( 0. ‘ 𝐾 )
lplnn0.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
Assertion lplnn0N ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ≠ 0 )

Proof

Step Hyp Ref Expression
1 lplnn0.z ⊢ 0 = ( 0. ‘ 𝐾 )
2 lplnn0.p ⊢ 𝑃 = ( LPlanes ‘ 𝐾 )
3 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
4 3 atex ⊢ ( 𝐾 ∈ HL → ( Atoms ‘ 𝐾 ) ≠ ∅ )
5 n0 ⊢ ( ( Atoms ‘ 𝐾 ) ≠ ∅ ↔ ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
6 4 5 sylib ⊢ ( 𝐾 ∈ HL → ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
7 6 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → ∃ 𝑝 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
8 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 8 3 2 lplnnleat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 )
10 9 3expa ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 )
11 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
12 11 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ OP )
13 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
14 13 3 atbase ⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
15 14 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
16 13 8 1 op0le ⊢ ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑝 )
17 12 15 16 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑝 )
18 breq1 ⊢ ( 𝑋 = 0 → ( 𝑋 ( le ‘ 𝐾 ) 𝑝 ↔ 0 ( le ‘ 𝐾 ) 𝑝 ) )
19 17 18 syl5ibrcom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑋 = 0 → 𝑋 ( le ‘ 𝐾 ) 𝑝 ) )
20 19 necon3bd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑋 ( le ‘ 𝐾 ) 𝑝 → 𝑋 ≠ 0 ) )
21 10 20 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑋 ≠ 0 )
22 7 21 exlimddv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ) → 𝑋 ≠ 0 )