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

Metamath Proof Explorer

Theorem lhpm0atN

Description: If the meet of a lattice hyperplane with a nonzero element is zero, the element is an atom. (Contributed by NM, 28-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lhpm0at.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lhpm0at.m ⊢ ∧ = ( meet ‘ 𝐾 )
lhpm0at.o ⊢ 0 = ( 0. ‘ 𝐾 )
lhpm0at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhpm0at.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpm0atN ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → 𝑋 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 lhpm0at.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lhpm0at.m ⊢ ∧ = ( meet ‘ 𝐾 )
3 lhpm0at.o ⊢ 0 = ( 0. ‘ 𝐾 )
4 lhpm0at.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 lhpm0at.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 simpr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → ( 𝑋 ∧ 𝑊 ) = 0 )
7 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 simpr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → 𝑋 ∈ 𝐵 )
9 simpr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → 𝑋 ≠ 0 )
10 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
11 10 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → 𝐾 ∈ Lat )
12 1 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵 )
13 12 ad2antlr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → 𝑊 ∈ 𝐵 )
14 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
15 1 14 2 latleeqm1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑊 ↔ ( 𝑋 ∧ 𝑊 ) = 𝑋 ) )
16 11 8 13 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑊 ↔ ( 𝑋 ∧ 𝑊 ) = 𝑋 ) )
17 16 biimpa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝑋 ∧ 𝑊 ) = 𝑋 )
18 simplr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → ( 𝑋 ∧ 𝑊 ) = 0 )
19 17 18 eqtr3d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) ∧ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) → 𝑋 = 0 )
20 19 ex ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑊 → 𝑋 = 0 ) )
21 20 necon3ad ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → ( 𝑋 ≠ 0 → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) )
22 9 21 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 )
23 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
24 1 14 2 23 5 lhpmcvr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝑋 ∧ 𝑊 ) ( ⋖ ‘ 𝐾 ) 𝑋 )
25 7 8 22 24 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → ( 𝑋 ∧ 𝑊 ) ( ⋖ ‘ 𝐾 ) 𝑋 )
26 6 25 eqbrtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → 0 ( ⋖ ‘ 𝐾 ) 𝑋 )
27 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → 𝐾 ∈ HL )
28 1 3 23 4 isat2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐴 ↔ 0 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
29 27 8 28 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → ( 𝑋 ∈ 𝐴 ↔ 0 ( ⋖ ‘ 𝐾 ) 𝑋 ) )
30 26 29 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ ( 𝑋 ∧ 𝑊 ) = 0 ) ) → 𝑋 ∈ 𝐴 )