atlen0

Description: A lattice element is nonzero if an atom is under it. (Contributed by NM, 26-May-2012)

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

Proof

Step	Hyp	Ref	Expression
1		atlen0.b	$⊢ B = {Base}_{K}$
2		atlen0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atlen0.z	$⊢ \underset{˙}{0} = 0. (K)$
4		atlen0.a	$⊢ A = Atoms (K)$
5		simpl1	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to K \in AtLat$
6	1 3	atl0cl	$⊢ K \in AtLat \to \underset{˙}{0} \in B$
7	5 6	syl	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to \underset{˙}{0} \in B$
8		simpl2	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to X \in B$
9	5 7 8	3jca	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to (K \in AtLat \land \underset{˙}{0} \in B \land X \in B)$
10		simpl3	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to P \in A$
11	1 4	atbase	$⊢ P \in A \to P \in B$
12	10 11	syl	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to P \in B$
13		eqid	$⊢ ⋖_{K} = ⋖_{K}$
14	3 13 4	atcvr0	$⊢ (K \in AtLat \land P \in A) \to \underset{˙}{0} ⋖_{K} P$
15	5 10 14	syl2anc	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to \underset{˙}{0} ⋖_{K} P$
16		eqid	$⊢ <_{K} = <_{K}$
17	1 16 13	cvrlt	$⊢ ((K \in AtLat \land \underset{˙}{0} \in B \land P \in B) \land \underset{˙}{0} ⋖_{K} P) \to \underset{˙}{0} <_{K} P$
18	5 7 12 15 17	syl31anc	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to \underset{˙}{0} <_{K} P$
19		simpr	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to P \underset{˙}{\leq} X$
20		atlpos	$⊢ K \in AtLat \to K \in Poset$
21	5 20	syl	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to K \in Poset$
22	1 2 16	pltletr	$⊢ (K \in Poset \land (\underset{˙}{0} \in B \land P \in B \land X \in B)) \to ((\underset{˙}{0} <_{K} P \land P \underset{˙}{\leq} X) \to \underset{˙}{0} <_{K} X)$
23	21 7 12 8 22	syl13anc	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to ((\underset{˙}{0} <_{K} P \land P \underset{˙}{\leq} X) \to \underset{˙}{0} <_{K} X)$
24	18 19 23	mp2and	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to \underset{˙}{0} <_{K} X$
25	16	pltne	$⊢ (K \in AtLat \land \underset{˙}{0} \in B \land X \in B) \to (\underset{˙}{0} <_{K} X \to \underset{˙}{0} \neq X)$
26	9 24 25	sylc	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to \underset{˙}{0} \neq X$
27	26	necomd	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land P \underset{˙}{\leq} X) \to X \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem atlen0

Proof