lncmp

Description: If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012)

	Ref	Expression
Hypotheses	lncmp.b	$⊢ B = {Base}_{K}$
	lncmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	lncmp.n	$⊢ N = Lines (K)$
	lncmp.m	$⊢ M = pmap (K)$
Assertion	lncmp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$

Proof

Step	Hyp	Ref	Expression
1		lncmp.b	$⊢ B = {Base}_{K}$
2		lncmp.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		lncmp.n	$⊢ N = Lines (K)$
4		lncmp.m	$⊢ M = pmap (K)$
5		simplrl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y) \to M (X) \in N$
6		simpll1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y) \to K \in HL$
7		simpll2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y) \to X \in B$
8		eqid	$⊢ join (K) = join (K)$
9		eqid	$⊢ Atoms (K) = Atoms (K)$
10	1 8 9 3 4	isline3	$⊢ (K \in HL \land X \in B) \to (M (X) \in N \leftrightarrow \exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land X = p join (K) q))$
11	6 7 10	syl2anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y) \to (M (X) \in N \leftrightarrow \exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land X = p join (K) q))$
12	5 11	mpbid	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y) \to \exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land X = p join (K) q)$
13		simp3rr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to X = p join (K) q$
14		simp1l1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to K \in HL$
15		simp1l3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to Y \in B$
16		simp1rr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to M (Y) \in N$
17		simp3ll	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to p \in Atoms (K)$
18		simp3lr	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to q \in Atoms (K)$
19		simp3rl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to p \neq q$
20	14	hllatd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to K \in Lat$
21	1 9	atbase	$⊢ p \in Atoms (K) \to p \in B$
22	17 21	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to p \in B$
23		simp1l2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to X \in B$
24	2 8 9	hlatlej1	$⊢ (K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \to p \underset{˙}{\leq} (p join (K) q)$
25	14 17 18 24	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to p \underset{˙}{\leq} (p join (K) q)$
26	25 13	breqtrrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to p \underset{˙}{\leq} X$
27		simp2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to X \underset{˙}{\leq} Y$
28	1 2 20 22 23 15 26 27	lattrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to p \underset{˙}{\leq} Y$
29	1 9	atbase	$⊢ q \in Atoms (K) \to q \in B$
30	18 29	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to q \in B$
31	2 8 9	hlatlej2	$⊢ (K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \to q \underset{˙}{\leq} (p join (K) q)$
32	14 17 18 31	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to q \underset{˙}{\leq} (p join (K) q)$
33	32 13	breqtrrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to q \underset{˙}{\leq} X$
34	1 2 20 30 23 15 33 27	lattrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to q \underset{˙}{\leq} Y$
35	1 2 8 9 3 4	lneq2at	$⊢ ((K \in HL \land Y \in B \land M (Y) \in N) \land (p \in Atoms (K) \land q \in Atoms (K) \land p \neq q) \land (p \underset{˙}{\leq} Y \land q \underset{˙}{\leq} Y)) \to Y = p join (K) q$
36	14 15 16 17 18 19 28 34 35	syl332anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to Y = p join (K) q$
37	13 36	eqtr4d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y \land ((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q))) \to X = Y$
38	37	3expia	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y) \to (((p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q)) \to X = Y)$
39	38	expd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y) \to ((p \in Atoms (K) \land q \in Atoms (K)) \to ((p \neq q \land X = p join (K) q) \to X = Y))$
40	39	rexlimdvv	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y) \to (\exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land X = p join (K) q) \to X = Y)$
41	12 40	mpd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \land X \underset{˙}{\leq} Y) \to X = Y$
42	41	ex	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \to (X \underset{˙}{\leq} Y \to X = Y)$
43		simpl1	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \to K \in HL$
44	43	hllatd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \to K \in Lat$
45		simpl2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \to X \in B$
46	1 2	latref	$⊢ (K \in Lat \land X \in B) \to X \underset{˙}{\leq} X$
47	44 45 46	syl2anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \to X \underset{˙}{\leq} X$
48		breq2	$⊢ X = Y \to (X \underset{˙}{\leq} X \leftrightarrow X \underset{˙}{\leq} Y)$
49	47 48	syl5ibcom	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \to (X = Y \to X \underset{˙}{\leq} Y)$
50	42 49	impbid	$⊢ ((K \in HL \land X \in B \land Y \in B) \land (M (X) \in N \land M (Y) \in N)) \to (X \underset{˙}{\leq} Y \leftrightarrow X = Y)$

Metamath Proof Explorer

Theorem lncmp

Proof