Theorem atnem0

Description: The meet of distinct atoms is zero. ( atnemeq0 analog.) (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atnem0.m	|- ./\ = ( meet ` K )
	atnem0.z	|- .0. = ( 0. ` K )
	atnem0.a	|- A = ( Atoms ` K )
Assertion	atnem0	|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> ( P ./\ Q ) = .0. ) )

Proof

Step	Hyp	Ref	Expression
1		atnem0.m	|- ./\ = ( meet ` K )
2		atnem0.z	|- .0. = ( 0. ` K )
3		atnem0.a	|- A = ( Atoms ` K )
4		eqid	|- ( le ` K ) = ( le ` K )
5	4 3	atncmp	|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( -. P ( le ` K ) Q <-> P =/= Q ) )
6		eqid	|- ( Base ` K ) = ( Base ` K )
7	6 3	atbase	|- ( Q e. A -> Q e. ( Base ` K ) )
8	6 4 1 2 3	atnle	|- ( ( K e. AtLat /\ P e. A /\ Q e. ( Base ` K ) ) -> ( -. P ( le ` K ) Q <-> ( P ./\ Q ) = .0. ) )
9	7 8	syl3an3	|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( -. P ( le ` K ) Q <-> ( P ./\ Q ) = .0. ) )
10	5 9	bitr3d	|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> ( P ./\ Q ) = .0. ) )