atcvreq0

Description: An element covered by an atom must be zero. ( atcveq0 analog.) (Contributed by NM, 4-Nov-2011)

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

Proof

Step	Hyp	Ref	Expression
1		atcvreq0.b	$⊢ B = {Base}_{K}$
2		atcvreq0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		atcvreq0.z	$⊢ \underset{˙}{0} = 0. (K)$
4		atcvreq0.c	$⊢ C = ⋖_{K}$
5		atcvreq0.a	$⊢ A = Atoms (K)$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7	1 6 3	atl0le	$⊢ (K \in AtLat \land X \in B) \to \underset{˙}{0} \leq_{K} X$
8	7	3adant3	$⊢ (K \in AtLat \land X \in B \land P \in A) \to \underset{˙}{0} \leq_{K} X$
9	8	adantr	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to \underset{˙}{0} \leq_{K} X$
10	1 5	atbase	$⊢ P \in A \to P \in B$
11		eqid	$⊢ <_{K} = <_{K}$
12	1 11 4	cvrlt	$⊢ ((K \in AtLat \land X \in B \land P \in B) \land X C P) \to X <_{K} P$
13	10 12	syl3anl3	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to X <_{K} P$
14		atlpos	$⊢ K \in AtLat \to K \in Poset$
15	14	3ad2ant1	$⊢ (K \in AtLat \land X \in B \land P \in A) \to K \in Poset$
16	15	adantr	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to K \in Poset$
17	1 3	atl0cl	$⊢ K \in AtLat \to \underset{˙}{0} \in B$
18	17	3ad2ant1	$⊢ (K \in AtLat \land X \in B \land P \in A) \to \underset{˙}{0} \in B$
19	18	adantr	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to \underset{˙}{0} \in B$
20	10	3ad2ant3	$⊢ (K \in AtLat \land X \in B \land P \in A) \to P \in B$
21	20	adantr	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to P \in B$
22		simpl2	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to X \in B$
23	3 4 5	atcvr0	$⊢ (K \in AtLat \land P \in A) \to \underset{˙}{0} C P$
24	23	3adant2	$⊢ (K \in AtLat \land X \in B \land P \in A) \to \underset{˙}{0} C P$
25	24	adantr	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to \underset{˙}{0} C P$
26	1 6 11 4	cvrnbtwn3	$⊢ (K \in Poset \land (\underset{˙}{0} \in B \land P \in B \land X \in B) \land \underset{˙}{0} C P) \to ((\underset{˙}{0} \leq_{K} X \land X <_{K} P) \leftrightarrow \underset{˙}{0} = X)$
27	16 19 21 22 25 26	syl131anc	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to ((\underset{˙}{0} \leq_{K} X \land X <_{K} P) \leftrightarrow \underset{˙}{0} = X)$
28	9 13 27	mpbi2and	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to \underset{˙}{0} = X$
29	28	eqcomd	$⊢ ((K \in AtLat \land X \in B \land P \in A) \land X C P) \to X = \underset{˙}{0}$
30	29	ex	$⊢ (K \in AtLat \land X \in B \land P \in A) \to (X C P \to X = \underset{˙}{0})$
31		breq1	$⊢ X = \underset{˙}{0} \to (X C P \leftrightarrow \underset{˙}{0} C P)$
32	24 31	syl5ibrcom	$⊢ (K \in AtLat \land X \in B \land P \in A) \to (X = \underset{˙}{0} \to X C P)$
33	30 32	impbid	$⊢ (K \in AtLat \land X \in B \land P \in A) \to (X C P \leftrightarrow X = \underset{˙}{0})$

Metamath Proof Explorer

Theorem atcvreq0

Proof