Metamath Proof Explorer

Theorem cvlatexch1

Description: Atom exchange property. (Contributed by NM, 5-Nov-2012)

		Ref	Expression
	Hypotheses	cvlatexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		cvlatexch.j	$⊢ \underset{˙}{\lor} = join (K)$
		cvlatexch.a	$⊢ A = Atoms (K)$
	Assertion	cvlatexch1	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{\leq} (R \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (R \underset{˙}{\lor} P))$

Proof

Step	Hyp	Ref	Expression
1		cvlatexch.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cvlatexch.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cvlatexch.a	$⊢ A = Atoms (K)$
4	1 2 3	cvlatexchb1	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{\leq} (R \underset{˙}{\lor} Q) \leftrightarrow R \underset{˙}{\lor} P = R \underset{˙}{\lor} Q)$
5		cvllat	$⊢ K \in CvLat \to K \in Lat$
6	5	3ad2ant1	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to K \in Lat$
7		simp23	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to R \in A$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
10	7 9	syl	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to R \in {Base}_{K}$
11		simp22	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to Q \in A$
12	8 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
13	11 12	syl	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to Q \in {Base}_{K}$
14	8 1 2	latlej2	$⊢ (K \in Lat \land R \in {Base}_{K} \land Q \in {Base}_{K}) \to Q \underset{˙}{\leq} (R \underset{˙}{\lor} Q)$
15	6 10 13 14	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to Q \underset{˙}{\leq} (R \underset{˙}{\lor} Q)$
16		breq2	$⊢ R \underset{˙}{\lor} P = R \underset{˙}{\lor} Q \to (Q \underset{˙}{\leq} (R \underset{˙}{\lor} P) \leftrightarrow Q \underset{˙}{\leq} (R \underset{˙}{\lor} Q))$
17	15 16	syl5ibrcom	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (R \underset{˙}{\lor} P = R \underset{˙}{\lor} Q \to Q \underset{˙}{\leq} (R \underset{˙}{\lor} P))$
18	4 17	sylbid	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{\leq} (R \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (R \underset{˙}{\lor} P))$