cvlatexchb2

Description: A version of cvlexchb2 for atoms. (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	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)$

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		simp22	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to Q \in A$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9	8 3	atbase	$⊢ Q \in A \to Q \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 Q \in {Base}_{K}$
11		simp23	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to R \in A$
12	8 3	atbase	$⊢ R \in A \to R \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 R \in {Base}_{K}$
14	8 2	latjcom	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\lor} R = 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{˙}{\lor} R = R \underset{˙}{\lor} Q$
16	15	breq2d	$⊢ (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{˙}{\leq} (R \underset{˙}{\lor} Q))$
17		simp21	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to P \in A$
18	8 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
19	17 18	syl	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to P \in {Base}_{K}$
20	8 2	latjcom	$⊢ (K \in Lat \land P \in {Base}_{K} \land R \in {Base}_{K}) \to P \underset{˙}{\lor} R = R \underset{˙}{\lor} P$
21	6 19 13 20	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to P \underset{˙}{\lor} R = R \underset{˙}{\lor} P$
22	21 15	eqeq12d	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq R) \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow R \underset{˙}{\lor} P = R \underset{˙}{\lor} Q)$
23	4 16 22	3bitr4d	$⊢ (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)$

Metamath Proof Explorer

Theorem cvlatexchb2

Proof