This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlexch4N

Description: A Hilbert lattice has the exchange property. Part of Definition 7.8 of MaedaMaeda p. 32. (Contributed by NM, 15-Nov-2011) (New usage is discouraged.)

		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	hlexch4N	$⊢ (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) \leftrightarrow X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$

Proof

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	cvlexch4N	$⊢ (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) \leftrightarrow X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$
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) \leftrightarrow X \underset{˙}{\lor} P = X \underset{˙}{\lor} Q)$