hlexch3

Description: A Hilbert lattice has the exchange property. ( atexch analog.) (Contributed by NM, 15-Nov-2011)

	Ref	Expression
Hypotheses	hlexch3.b	$⊢ B = {Base}_{K}$
	hlexch3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	hlexch3.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlexch3.m	$⊢ \underset{˙}{\land} = meet (K)$
	hlexch3.z	$⊢ \underset{˙}{0} = 0. (K)$
	hlexch3.a	$⊢ A = Atoms (K)$
Assertion	hlexch3	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land P \underset{˙}{\land} X = \underset{˙}{0}) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (X \underset{˙}{\lor} P))$

Step	Hyp	Ref	Expression
1		hlexch3.b	$⊢ B = {Base}_{K}$
2		hlexch3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		hlexch3.j	$⊢ \underset{˙}{\lor} = join (K)$
4		hlexch3.m	$⊢ \underset{˙}{\land} = meet (K)$
5		hlexch3.z	$⊢ \underset{˙}{0} = 0. (K)$
6		hlexch3.a	$⊢ A = Atoms (K)$
7		hlcvl	$⊢ K \in HL \to K \in CvLat$
8	1 2 3 4 5 6	cvlexch3	$⊢ (K \in CvLat \land (P \in A \land Q \in A \land X \in B) \land P \underset{˙}{\land} X = \underset{˙}{0}) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (X \underset{˙}{\lor} P))$
9	7 8	syl3an1	$⊢ (K \in HL \land (P \in A \land Q \in A \land X \in B) \land P \underset{˙}{\land} X = \underset{˙}{0}) \to (P \underset{˙}{\leq} (X \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (X \underset{˙}{\lor} P))$

Metamath Proof Explorer