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 )