cvlsupr7

Description: Consequence of superposition condition ( P .\/ R ) = ( Q .\/ R ) . (Contributed by NM, 24-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cvlsupr5.a	$⊢ A = Atoms (K)$
2		cvlsupr5.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cvllat	$⊢ K \in CvLat \to K \in Lat$
4	3	3ad2ant1	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to K \in Lat$
5		simp21	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \in A$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 1	atbase	$⊢ P \in A \to P \in {Base}_{K}$
8	5 7	syl	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \in {Base}_{K}$
9		simp23	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to R \in A$
10	6 1	atbase	$⊢ R \in A \to R \in {Base}_{K}$
11	9 10	syl	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to R \in {Base}_{K}$
12		eqid	$⊢ \leq_{K} = \leq_{K}$
13	6 12 2	latlej1	$⊢ (K \in Lat \land P \in {Base}_{K} \land R \in {Base}_{K}) \to P \leq_{K} (P \underset{˙}{\lor} R)$
14	4 8 11 13	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \leq_{K} (P \underset{˙}{\lor} R)$
15		simp3r	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R$
16	14 15	breqtrd	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \leq_{K} (Q \underset{˙}{\lor} R)$
17		simp22	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to Q \in A$
18	6 1	atbase	$⊢ Q \in A \to Q \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 Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to Q \in {Base}_{K}$
20	6 2	latjcom	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R \in {Base}_{K}) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
21	4 19 11 20	syl3anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to Q \underset{˙}{\lor} R = R \underset{˙}{\lor} Q$
22	16 21	breqtrd	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \leq_{K} (R \underset{˙}{\lor} Q)$
23		simp1	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to K \in CvLat$
24		simp3l	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \neq Q$
25	12 2 1	cvlatexchb2	$⊢ (K \in CvLat \land (P \in A \land R \in A \land Q \in A) \land P \neq Q) \to (P \leq_{K} (R \underset{˙}{\lor} Q) \leftrightarrow P \underset{˙}{\lor} Q = R \underset{˙}{\lor} Q)$
26	23 5 9 17 24 25	syl131anc	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to (P \leq_{K} (R \underset{˙}{\lor} Q) \leftrightarrow P \underset{˙}{\lor} Q = R \underset{˙}{\lor} Q)$
27	22 26	mpbid	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q = R \underset{˙}{\lor} Q$

Metamath Proof Explorer

Theorem cvlsupr7

Proof