cvlatexch3

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

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		simp1	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \to K \in CvLat$
5		simp21	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \to P \in A$
6		simp23	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \to R \in A$
7		simp22	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \to Q \in A$
8		simp3l	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \to P \neq Q$
9	1 2 3	cvlatexchb1	$⊢ (K \in CvLat \land (P \in A \land R \in A \land Q \in A) \land P \neq Q) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow Q \underset{˙}{\lor} P = Q \underset{˙}{\lor} R)$
10	4 5 6 7 8 9	syl131anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow Q \underset{˙}{\lor} P = Q \underset{˙}{\lor} R)$
11	10	biimpa	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to Q \underset{˙}{\lor} P = Q \underset{˙}{\lor} R$
12		simpl1	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to K \in CvLat$
13		cvllat	$⊢ K \in CvLat \to K \in Lat$
14	12 13	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to K \in Lat$
15		simpl21	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to P \in A$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17	16 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
18	15 17	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to P \in {Base}_{K}$
19		simpl22	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to Q \in A$
20	16 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
21	19 20	syl	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to Q \in {Base}_{K}$
22	16 2	latjcom	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
23	14 18 21 22	syl3anc	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
24	1 2 3	cvlatexchb2	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
25	24	3adant3l	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \leftrightarrow P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)$
26	25	biimpa	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
27	11 23 26	3eqtr4d	$⊢ ((K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \land P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R$
28	27	ex	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \neq R)) \to (P \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \to P \underset{˙}{\lor} Q = P \underset{˙}{\lor} R)$

Metamath Proof Explorer

Theorem cvlatexch3

Proof