atcmp

Description: If two atoms are comparable, they are equal. ( atsseq analog.) (Contributed by NM, 13-Oct-2011)

	Ref	Expression
Hypotheses	atcmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	atcmp.a	$⊢ A = Atoms (K)$
Assertion	atcmp	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \underset{˙}{\leq} Q \leftrightarrow P = Q)$

Step	Hyp	Ref	Expression
1		atcmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		atcmp.a	$⊢ A = Atoms (K)$
3		atlpos	$⊢ K \in AtLat \to K \in Poset$
4	3	3ad2ant1	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to K \in Poset$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6	5 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
7	6	3ad2ant2	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to P \in {Base}_{K}$
8	5 2	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
9	8	3ad2ant3	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to Q \in {Base}_{K}$
10		eqid	$⊢ 0. (K) = 0. (K)$
11	5 10	atl0cl	$⊢ K \in AtLat \to 0. (K) \in {Base}_{K}$
12	11	3ad2ant1	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to 0. (K) \in {Base}_{K}$
13		eqid	$⊢ ⋖_{K} = ⋖_{K}$
14	10 13 2	atcvr0	$⊢ (K \in AtLat \land P \in A) \to 0. (K) ⋖_{K} P$
15	14	3adant3	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to 0. (K) ⋖_{K} P$
16	10 13 2	atcvr0	$⊢ (K \in AtLat \land Q \in A) \to 0. (K) ⋖_{K} Q$
17	16	3adant2	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to 0. (K) ⋖_{K} Q$
18	5 1 13	cvrcmp	$⊢ (K \in Poset \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land 0. (K) \in {Base}_{K}) \land (0. (K) ⋖_{K} P \land 0. (K) ⋖_{K} Q)) \to (P \underset{˙}{\leq} Q \leftrightarrow P = Q)$
19	4 7 9 12 15 17 18	syl132anc	$⊢ (K \in AtLat \land P \in A \land Q \in A) \to (P \underset{˙}{\leq} Q \leftrightarrow P = Q)$

Metamath Proof Explorer