llncmp

Description: If two lattice lines are comparable, they are equal. (Contributed by NM, 19-Jun-2012)

	Ref	Expression
Hypotheses	llncmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	llncmp.n	$⊢ N = LLines (K)$
Assertion	llncmp	$⊢ (K \in HL \land X \in N \land Y \in N) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		llncmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		llncmp.n	$⊢ N = LLines (K)$
3		simp2	$⊢ (K \in HL \land X \in N \land Y \in N) \to X \in N$
4		simp1	$⊢ (K \in HL \land X \in N \land Y \in N) \to K \in HL$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6	5 2	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
7	6	3ad2ant2	$⊢ (K \in HL \land X \in N \land Y \in N) \to X \in {Base}_{K}$
8		eqid	$⊢ ⋖_{K} = ⋖_{K}$
9		eqid	$⊢ Atoms (K) = Atoms (K)$
10	5 8 9 2	islln4	$⊢ (K \in HL \land X \in {Base}_{K}) \to (X \in N \leftrightarrow \exists p \in Atoms (K) p ⋖_{K} X)$
11	4 7 10	syl2anc	$⊢ (K \in HL \land X \in N \land Y \in N) \to (X \in N \leftrightarrow \exists p \in Atoms (K) p ⋖_{K} X)$
12	3 11	mpbid	$⊢ (K \in HL \land X \in N \land Y \in N) \to \exists p \in Atoms (K) p ⋖_{K} X$
13		simpr3	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to X \underset{˙}{\leq} Y$
14		hlpos	$⊢ K \in HL \to K \in Poset$
15	14	3ad2ant1	$⊢ (K \in HL \land X \in N \land Y \in N) \to K \in Poset$
16	15	adantr	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to K \in Poset$
17	7	adantr	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to X \in {Base}_{K}$
18		simpl3	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to Y \in N$
19	5 2	llnbase	$⊢ Y \in N \to Y \in {Base}_{K}$
20	18 19	syl	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to Y \in {Base}_{K}$
21		simpr1	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to p \in Atoms (K)$
22	5 9	atbase	$⊢ p \in Atoms (K) \to p \in {Base}_{K}$
23	21 22	syl	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to p \in {Base}_{K}$
24		simpr2	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to p ⋖_{K} X$
25		simpl1	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to K \in HL$
26	5 1 8	cvrle	$⊢ ((K \in HL \land p \in {Base}_{K} \land X \in {Base}_{K}) \land p ⋖_{K} X) \to p \underset{˙}{\leq} X$
27	25 23 17 24 26	syl31anc	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to p \underset{˙}{\leq} X$
28	5 1	postr	$⊢ (K \in Poset \land (p \in {Base}_{K} \land X \in {Base}_{K} \land Y \in {Base}_{K})) \to ((p \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \to p \underset{˙}{\leq} Y)$
29	16 23 17 20 28	syl13anc	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to ((p \underset{˙}{\leq} X \land X \underset{˙}{\leq} Y) \to p \underset{˙}{\leq} Y)$
30	27 13 29	mp2and	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to p \underset{˙}{\leq} Y$
31	1 8 9 2	atcvrlln2	$⊢ ((K \in HL \land p \in Atoms (K) \land Y \in N) \land p \underset{˙}{\leq} Y) \to p ⋖_{K} Y$
32	25 21 18 30 31	syl31anc	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to p ⋖_{K} Y$
33	5 1 8	cvrcmp	$⊢ (K \in Poset \land (X \in {Base}_{K} \land Y \in {Base}_{K} \land p \in {Base}_{K}) \land (p ⋖_{K} X \land p ⋖_{K} Y)) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$
34	16 17 20 23 24 32 33	syl132anc	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$
35	13 34	mpbid	$⊢ ((K \in HL \land X \in N \land Y \in N) \land (p \in Atoms (K) \land p ⋖_{K} X \land X \underset{˙}{\leq} Y)) \to X = Y$
36	35	3exp2	$⊢ (K \in HL \land X \in N \land Y \in N) \to (p \in Atoms (K) \to (p ⋖_{K} X \to (X \underset{˙}{\leq} Y \to X = Y)))$
37	36	rexlimdv	$⊢ (K \in HL \land X \in N \land Y \in N) \to (\exists p \in Atoms (K) p ⋖_{K} X \to (X \underset{˙}{\leq} Y \to X = Y))$
38	12 37	mpd	$⊢ (K \in HL \land X \in N \land Y \in N) \to (X \underset{˙}{\leq} Y \to X = Y)$
39	5 1	posref	$⊢ (K \in Poset \land X \in {Base}_{K}) \to X \underset{˙}{\leq} X$
40	15 7 39	syl2anc	$⊢ (K \in HL \land X \in N \land Y \in N) \to X \underset{˙}{\leq} X$
41		breq2	$⊢ X = Y \to (X \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{\leq} Y)$
42	40 41	syl5ibcom	$⊢ (K \in HL \land X \in N \land Y \in N) \to (X = Y \to X \underset{˙}{\leq} Y)$
43	38 42	impbid	$⊢ (K \in HL \land X \in N \land Y \in N) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem llncmp

Proof