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 ) ) → 𝑋 ∈ 𝐴 )