Metamath Proof Explorer

Theorem cvlsupr8

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	cvlsupr8	$⊢ (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 = P \underset{˙}{\lor} R$

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		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$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 1	atbase	$⊢ Q \in A \to Q \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 Q \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	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$
13	4 8 11 12	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$
14		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$
15	1 2	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$
16	13 14 15	3eqtr4rd	$⊢ (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 = P \underset{˙}{\lor} R$