cvlsupr5

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

	Ref	Expression
Hypotheses	cvlsupr5.a	$⊢ A = Atoms (K)$
	cvlsupr5.j	$⊢ \underset{˙}{\lor} = join (K)$
Assertion	cvlsupr5	$⊢ (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 \neq P$

Step	Hyp	Ref	Expression
1		cvlsupr5.a	$⊢ A = Atoms (K)$
2		cvlsupr5.j	$⊢ \underset{˙}{\lor} = join (K)$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4	1 3 2	cvlsupr2	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \leftrightarrow (R \neq P \land R \neq Q \land R \leq_{K} (P \underset{˙}{\lor} Q)))$
5		simp1	$⊢ (R \neq P \land R \neq Q \land R \leq_{K} (P \underset{˙}{\lor} Q)) \to R \neq P$
6	4 5	biimtrdi	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land R \in A) \land P \neq Q) \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \to R \neq P)$
7	6	3exp	$⊢ K \in CvLat \to ((P \in A \land Q \in A \land R \in A) \to (P \neq Q \to (P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R \to R \neq P)))$
8	7	imp4a	$⊢ K \in CvLat \to ((P \in A \land Q \in A \land R \in A) \to ((P \neq Q \land P \underset{˙}{\lor} R = Q \underset{˙}{\lor} R) \to R \neq P))$
9	8	3imp	$⊢ (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 \neq P$

Metamath Proof Explorer