atnle

Description: Two ways of expressing "an atom is not less than or equal to a lattice element." ( atnssm0 analog.) (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Hypotheses	atnle.b	$⊢ B = {Base}_{K}$
	atnle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atnle.m	$⊢ \underset{˙}{\land} = meet (K)$
	atnle.z	$⊢ \underset{˙}{0} = 0. (K)$
	atnle.a	$⊢ A = Atoms (K)$
Assertion	atnle	$⊢ (K \in AtLat \land P \in A \land X \in B) \to (\neg P \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\land} X = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		atnle.b	$⊢ B = {Base}_{K}$
2		atnle.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atnle.m	$⊢ \underset{˙}{\land} = meet (K)$
4		atnle.z	$⊢ \underset{˙}{0} = 0. (K)$
5		atnle.a	$⊢ A = Atoms (K)$
6		simpl1	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X \neq \underset{˙}{0}) \to K \in AtLat$
7		atllat	$⊢ K \in AtLat \to K \in Lat$
8	7	3ad2ant1	$⊢ (K \in AtLat \land P \in A \land X \in B) \to K \in Lat$
9	1 5	atbase	$⊢ P \in A \to P \in B$
10	9	3ad2ant2	$⊢ (K \in AtLat \land P \in A \land X \in B) \to P \in B$
11		simp3	$⊢ (K \in AtLat \land P \in A \land X \in B) \to X \in B$
12	1 3	latmcl	$⊢ (K \in Lat \land P \in B \land X \in B) \to P \underset{˙}{\land} X \in B$
13	8 10 11 12	syl3anc	$⊢ (K \in AtLat \land P \in A \land X \in B) \to P \underset{˙}{\land} X \in B$
14	13	adantr	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X \neq \underset{˙}{0}) \to P \underset{˙}{\land} X \in B$
15		simpr	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X \neq \underset{˙}{0}) \to P \underset{˙}{\land} X \neq \underset{˙}{0}$
16	1 2 4 5	atlex	$⊢ (K \in AtLat \land P \underset{˙}{\land} X \in B \land P \underset{˙}{\land} X \neq \underset{˙}{0}) \to \exists y \in A y \underset{˙}{\leq} (P \underset{˙}{\land} X)$
17	6 14 15 16	syl3anc	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X \neq \underset{˙}{0}) \to \exists y \in A y \underset{˙}{\leq} (P \underset{˙}{\land} X)$
18		simpl1	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to K \in AtLat$
19	18 7	syl	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to K \in Lat$
20	1 5	atbase	$⊢ y \in A \to y \in B$
21	20	adantl	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to y \in B$
22		simpl2	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to P \in A$
23	22 9	syl	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to P \in B$
24		simpl3	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to X \in B$
25	1 2 3	latlem12	$⊢ (K \in Lat \land (y \in B \land P \in B \land X \in B)) \to ((y \underset{˙}{\leq} P \land y \underset{˙}{\leq} X) \leftrightarrow y \underset{˙}{\leq} (P \underset{˙}{\land} X))$
26	19 21 23 24 25	syl13anc	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to ((y \underset{˙}{\leq} P \land y \underset{˙}{\leq} X) \leftrightarrow y \underset{˙}{\leq} (P \underset{˙}{\land} X))$
27		simpr	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to y \in A$
28	2 5	atcmp	$⊢ (K \in AtLat \land y \in A \land P \in A) \to (y \underset{˙}{\leq} P \leftrightarrow y = P)$
29	18 27 22 28	syl3anc	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to (y \underset{˙}{\leq} P \leftrightarrow y = P)$
30		breq1	$⊢ y = P \to (y \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\leq} X)$
31	30	biimpd	$⊢ y = P \to (y \underset{˙}{\leq} X \to P \underset{˙}{\leq} X)$
32	29 31	biimtrdi	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to (y \underset{˙}{\leq} P \to (y \underset{˙}{\leq} X \to P \underset{˙}{\leq} X))$
33	32	impd	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to ((y \underset{˙}{\leq} P \land y \underset{˙}{\leq} X) \to P \underset{˙}{\leq} X)$
34	26 33	sylbird	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land y \in A) \to (y \underset{˙}{\leq} (P \underset{˙}{\land} X) \to P \underset{˙}{\leq} X)$
35	34	adantlr	$⊢ (((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X \neq \underset{˙}{0}) \land y \in A) \to (y \underset{˙}{\leq} (P \underset{˙}{\land} X) \to P \underset{˙}{\leq} X)$
36	35	rexlimdva	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X \neq \underset{˙}{0}) \to (\exists y \in A y \underset{˙}{\leq} (P \underset{˙}{\land} X) \to P \underset{˙}{\leq} X)$
37	17 36	mpd	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X \neq \underset{˙}{0}) \to P \underset{˙}{\leq} X$
38	37	ex	$⊢ (K \in AtLat \land P \in A \land X \in B) \to (P \underset{˙}{\land} X \neq \underset{˙}{0} \to P \underset{˙}{\leq} X)$
39	38	necon1bd	$⊢ (K \in AtLat \land P \in A \land X \in B) \to (\neg P \underset{˙}{\leq} X \to P \underset{˙}{\land} X = \underset{˙}{0})$
40	4 5	atn0	$⊢ (K \in AtLat \land P \in A) \to P \neq \underset{˙}{0}$
41	40	3adant3	$⊢ (K \in AtLat \land P \in A \land X \in B) \to P \neq \underset{˙}{0}$
42	1 2 3	latleeqm1	$⊢ (K \in Lat \land P \in B \land X \in B) \to (P \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\land} X = P)$
43	8 10 11 42	syl3anc	$⊢ (K \in AtLat \land P \in A \land X \in B) \to (P \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\land} X = P)$
44	43	adantr	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X = \underset{˙}{0}) \to (P \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\land} X = P)$
45		eqeq1	$⊢ P \underset{˙}{\land} X = P \to (P \underset{˙}{\land} X = \underset{˙}{0} \leftrightarrow P = \underset{˙}{0})$
46	45	biimpcd	$⊢ P \underset{˙}{\land} X = \underset{˙}{0} \to (P \underset{˙}{\land} X = P \to P = \underset{˙}{0})$
47	46	adantl	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X = \underset{˙}{0}) \to (P \underset{˙}{\land} X = P \to P = \underset{˙}{0})$
48	44 47	sylbid	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X = \underset{˙}{0}) \to (P \underset{˙}{\leq} X \to P = \underset{˙}{0})$
49	48	necon3ad	$⊢ ((K \in AtLat \land P \in A \land X \in B) \land P \underset{˙}{\land} X = \underset{˙}{0}) \to (P \neq \underset{˙}{0} \to \neg P \underset{˙}{\leq} X)$
50	49	ex	$⊢ (K \in AtLat \land P \in A \land X \in B) \to (P \underset{˙}{\land} X = \underset{˙}{0} \to (P \neq \underset{˙}{0} \to \neg P \underset{˙}{\leq} X))$
51	41 50	mpid	$⊢ (K \in AtLat \land P \in A \land X \in B) \to (P \underset{˙}{\land} X = \underset{˙}{0} \to \neg P \underset{˙}{\leq} X)$
52	39 51	impbid	$⊢ (K \in AtLat \land P \in A \land X \in B) \to (\neg P \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\land} X = \underset{˙}{0})$

Metamath Proof Explorer

Theorem atnle

Proof