cvlexchb1

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011)

	Ref	Expression
Hypotheses	cvlexch.b	$⊢ B = {Base}_{K}$
	cvlexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cvlexch.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvlexch.a	$⊢ A = Atoms (K)$
Assertion	cvlexchb1	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \leftrightarrow X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$

Proof

Step	Hyp	Ref	Expression
1		cvlexch.b	$⊢ B = {Base}_{K}$
2		cvlexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvlexch.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cvlexch.a	$⊢ A = Atoms (K)$
5		cvllat	$⊢ K \in CvLat \to K \in Lat$
6	5	adantr	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to K \in Lat$
7		simpr3	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to X \in B$
8		simpr2	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to Q \in A$
9	1 4	atbase	$⊢ Q \in A \to Q \in B$
10	8 9	syl	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to Q \in B$
11	1 2 3	latlej1	$⊢ (K \in Lat \land X \in B \land Q \in B) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
12	6 7 10 11	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
13	12	3adant3	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
14	13	adantr	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
15		simpr	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
16		simpr1	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to P \in A$
17	1 4	atbase	$⊢ P \in A \to P \in B$
18	16 17	syl	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to P \in B$
19	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land Q \in B) \to X \underset{˙}{\lor} Q \in B$
20	6 7 10 19	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to X \underset{˙}{\lor} Q \in B$
21	1 2 3	latjle12	$⊢ (K \in Lat \land (X \in B \land P \in B \land X \underset{˙}{\lor} Q \in B)) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \leftrightarrow (X \underset{˙}{\lor} P) \underset{˙}{\leq} (X \underset{˙}{\lor} Q))$
22	6 7 18 20 21	syl13anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \leftrightarrow (X \underset{˙}{\lor} P) \underset{˙}{\leq} (X \underset{˙}{\lor} Q))$
23	22	3adant3	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \leftrightarrow (X \underset{˙}{\lor} P) \underset{˙}{\leq} (X \underset{˙}{\lor} Q))$
24	23	adantr	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \leftrightarrow (X \underset{˙}{\lor} P) \underset{˙}{\leq} (X \underset{˙}{\lor} Q))$
25	14 15 24	mpbi2and	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to (X \underset{˙}{\lor} P) \underset{˙}{\leq} (X \underset{˙}{\lor} Q)$
26	1 2 3	latlej1	$⊢ (K \in Lat \land X \in B \land P \in B) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} P)$
27	6 7 18 26	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} P)$
28	27	3adant3	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} P)$
29	28	adantr	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to X \underset{˙}{\leq} (X \underset{˙}{\lor} P)$
30	1 2 3 4	cvlexch1	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (X \underset{˙}{\lor} P))$
31	30	imp	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to Q \underset{˙}{\leq} (X \underset{˙}{\lor} P)$
32	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land P \in B) \to X \underset{˙}{\lor} P \in B$
33	6 7 18 32	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to X \underset{˙}{\lor} P \in B$
34	1 2 3	latjle12	$⊢ (K \in Lat \land (X \in B \land Q \in B \land X \underset{˙}{\lor} P \in B)) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} P) \land Q \underset{˙}{\leq} (X \underset{˙}{\lor} P)) \leftrightarrow (X \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} P))$
35	6 7 10 33 34	syl13anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} P) \land Q \underset{˙}{\leq} (X \underset{˙}{\lor} P)) \leftrightarrow (X \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} P))$
36	35	3adant3	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} P) \land Q \underset{˙}{\leq} (X \underset{˙}{\lor} P)) \leftrightarrow (X \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} P))$
37	36	adantr	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} P) \land Q \underset{˙}{\leq} (X \underset{˙}{\lor} P)) \leftrightarrow (X \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} P))$
38	29 31 37	mpbi2and	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to (X \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} P)$
39	1 2	latasymb	$⊢ (K \in Lat \land X \underset{˙}{\lor} P \in B \land X \underset{˙}{\lor} Q \in B) \to (((X \underset{˙}{\lor} P) \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \land (X \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} P)) \leftrightarrow X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$
40	6 33 20 39	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to (((X \underset{˙}{\lor} P) \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \land (X \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} P)) \leftrightarrow X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$
41	40	3adant3	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to (((X \underset{˙}{\lor} P) \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \land (X \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} P)) \leftrightarrow X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$
42	41	adantr	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to (((X \underset{˙}{\lor} P) \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \land (X \underset{˙}{\lor} Q) \underset{˙}{\leq} (X \underset{˙}{\lor} P)) \leftrightarrow X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$
43	25 38 42	mpbi2and	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \land P \underset{˙}{\leq} (X \underset{˙}{\lor} Q)) \to X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q$
44	43	ex	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$
45	1 2 3	latlej2	$⊢ (K \in Lat \land X \in B \land P \in B) \to P \underset{˙}{\leq} (X \underset{˙}{\lor} P)$
46	6 7 18 45	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to P \underset{˙}{\leq} (X \underset{˙}{\lor} P)$
47		breq2	$⊢ X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} P) \leftrightarrow P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))$
48	46 47	syl5ibcom	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B)) \to (X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q \to P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))$
49	48	3adant3	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to (X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q \to P \underset{˙}{\leq} (X \underset{˙}{\lor} Q))$
50	44 49	impbid	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land \neg P \underset{˙}{\leq} X) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \leftrightarrow X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$

Metamath Proof Explorer

Theorem cvlexchb1

Proof