atltcvr

Description: An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012)

	Ref	Expression
Hypotheses	atltcvr.s	$⊢ \underset{˙}{<} = <_{K}$
	atltcvr.j	$⊢ \underset{˙}{\lor} = join (K)$
	atltcvr.a	$⊢ A = Atoms (K)$
	atltcvr.c	$⊢ C = ⋖_{K}$
Assertion	atltcvr	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \leftrightarrow P C (Q \underset{˙}{\lor} R))$

Proof

Step	Hyp	Ref	Expression
1		atltcvr.s	$⊢ \underset{˙}{<} = <_{K}$
2		atltcvr.j	$⊢ \underset{˙}{\lor} = join (K)$
3		atltcvr.a	$⊢ A = Atoms (K)$
4		atltcvr.c	$⊢ C = ⋖_{K}$
5		oveq1	$⊢ Q = R \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} R$
6		simpr3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in A$
7	2 3	hlatjidm	$⊢ (K \in HL \land R \in A) \to R \underset{˙}{\lor} R = R$
8	6 7	syldan	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \underset{˙}{\lor} R = R$
9	5 8	sylan9eqr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land Q = R) \to Q \underset{˙}{\lor} R = R$
10	9	breq2d	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land Q = R) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{<} R)$
11		hlatl	$⊢ K \in HL \to K \in AtLat$
12	11	adantr	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in AtLat$
13		simpr1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \in A$
14	1 3	atnlt	$⊢ (K \in AtLat \land P \in A \land R \in A) \to \neg P \underset{˙}{<} R$
15	12 13 6 14	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to \neg P \underset{˙}{<} R$
16	15	pm2.21d	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{<} R \to P C (Q \underset{˙}{\lor} R))$
17	16	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land Q = R) \to (P \underset{˙}{<} R \to P C (Q \underset{˙}{\lor} R))$
18	10 17	sylbid	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land Q = R) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \to P C (Q \underset{˙}{\lor} R))$
19		simpl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in HL$
20		hllat	$⊢ K \in HL \to K \in Lat$
21	20	adantr	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in Lat$
22		simpr2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to Q \in A$
23		eqid	$⊢ {Base}_{K} = {Base}_{K}$
24	23 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
25	22 24	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to Q \in {Base}_{K}$
26	23 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
27	6 26	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in {Base}_{K}$
28	23 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
29	21 25 27 28	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to Q \underset{˙}{\lor} R \in {Base}_{K}$
30		eqid	$⊢ \leq_{K} = \leq_{K}$
31	30 1	pltle	$⊢ (K \in HL \land P \in A \land Q \underset{˙}{\lor} R \in {Base}_{K}) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \to P \leq_{K} (Q \underset{˙}{\lor} R))$
32	19 13 29 31	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \to P \leq_{K} (Q \underset{˙}{\lor} R))$
33	32	adantr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land Q \neq R) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \to P \leq_{K} (Q \underset{˙}{\lor} R))$
34		simpll	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land (Q \neq R \land P \leq_{K} (Q \underset{˙}{\lor} R))) \to K \in HL$
35		simplr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land (Q \neq R \land P \leq_{K} (Q \underset{˙}{\lor} R))) \to (P \in A \land Q \in A \land R \in A)$
36		simpr	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land (Q \neq R \land P \leq_{K} (Q \underset{˙}{\lor} R))) \to (Q \neq R \land P \leq_{K} (Q \underset{˙}{\lor} R))$
37	34 35 36	3jca	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land (Q \neq R \land P \leq_{K} (Q \underset{˙}{\lor} R))) \to (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \leq_{K} (Q \underset{˙}{\lor} R)))$
38	37	anassrs	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land Q \neq R) \land P \leq_{K} (Q \underset{˙}{\lor} R)) \to (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \leq_{K} (Q \underset{˙}{\lor} R)))$
39	30 2 4 3	atcvrj2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (Q \neq R \land P \leq_{K} (Q \underset{˙}{\lor} R))) \to P C (Q \underset{˙}{\lor} R)$
40	38 39	syl	$⊢ (((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land Q \neq R) \land P \leq_{K} (Q \underset{˙}{\lor} R)) \to P C (Q \underset{˙}{\lor} R)$
41	40	ex	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land Q \neq R) \to (P \leq_{K} (Q \underset{˙}{\lor} R) \to P C (Q \underset{˙}{\lor} R))$
42	33 41	syld	$⊢ ((K \in HL \land (P \in A \land Q \in A \land R \in A)) \land Q \neq R) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \to P C (Q \underset{˙}{\lor} R))$
43	18 42	pm2.61dane	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \to P C (Q \underset{˙}{\lor} R))$
44	23 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
45	13 44	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \in {Base}_{K}$
46	23 1 4	cvrlt	$⊢ ((K \in HL \land P \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K}) \land P C (Q \underset{˙}{\lor} R)) \to P \underset{˙}{<} (Q \underset{˙}{\lor} R)$
47	46	ex	$⊢ (K \in HL \land P \in {Base}_{K} \land Q \underset{˙}{\lor} R \in {Base}_{K}) \to (P C (Q \underset{˙}{\lor} R) \to P \underset{˙}{<} (Q \underset{˙}{\lor} R))$
48	19 45 29 47	syl3anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P C (Q \underset{˙}{\lor} R) \to P \underset{˙}{<} (Q \underset{˙}{\lor} R))$
49	43 48	impbid	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{<} (Q \underset{˙}{\lor} R) \leftrightarrow P C (Q \underset{˙}{\lor} R))$

Metamath Proof Explorer

Theorem atltcvr

Proof