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

Metamath Proof Explorer

Theorem ishlatiN

Description: Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	ishlati.1	$⊢ K \in OML$
		ishlati.2	$⊢ K \in CLat$
		ishlati.3	$⊢ K \in AtLat$
		ishlati.b	$⊢ B = {Base}_{K}$
		ishlati.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		ishlati.s	$⊢ \underset{˙}{<} = <_{K}$
		ishlati.j	$⊢ \underset{˙}{\lor} = join (K)$
		ishlati.z	$⊢ \underset{˙}{0} = 0. (K)$
		ishlati.u	$⊢ \underset{˙}{1} = 1. (K)$
		ishlati.a	$⊢ A = Atoms (K)$
		ishlati.9	$⊢ \forall x \in A \forall y \in A ((x \neq y \to \exists z \in A (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land \forall z \in B ((\neg x \underset{˙}{\leq} z \land x \underset{˙}{\leq} (z \underset{˙}{\lor} y)) \to y \underset{˙}{\leq} (z \underset{˙}{\lor} x)))$
		ishlati.10	$⊢ \exists x \in B \exists y \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}))$
	Assertion	ishlatiN	$⊢ K \in HL$

Proof

Step	Hyp	Ref	Expression
1		ishlati.1	$⊢ K \in OML$
2		ishlati.2	$⊢ K \in CLat$
3		ishlati.3	$⊢ K \in AtLat$
4		ishlati.b	$⊢ B = {Base}_{K}$
5		ishlati.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
6		ishlati.s	$⊢ \underset{˙}{<} = <_{K}$
7		ishlati.j	$⊢ \underset{˙}{\lor} = join (K)$
8		ishlati.z	$⊢ \underset{˙}{0} = 0. (K)$
9		ishlati.u	$⊢ \underset{˙}{1} = 1. (K)$
10		ishlati.a	$⊢ A = Atoms (K)$
11		ishlati.9	$⊢ \forall x \in A \forall y \in A ((x \neq y \to \exists z \in A (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land \forall z \in B ((\neg x \underset{˙}{\leq} z \land x \underset{˙}{\leq} (z \underset{˙}{\lor} y)) \to y \underset{˙}{\leq} (z \underset{˙}{\lor} x)))$
12		ishlati.10	$⊢ \exists x \in B \exists y \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}))$
13	1 2 3	3pm3.2i	$⊢ (K \in OML \land K \in CLat \land K \in AtLat)$
14	11 12	pm3.2i	$⊢ (\forall x \in A \forall y \in A ((x \neq y \to \exists z \in A (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land \forall z \in B ((\neg x \underset{˙}{\leq} z \land x \underset{˙}{\leq} (z \underset{˙}{\lor} y)) \to y \underset{˙}{\leq} (z \underset{˙}{\lor} x))) \land \exists x \in B \exists y \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1})))$
15	4 5 6 7 8 9 10	ishlat2	$⊢ K \in HL \leftrightarrow ((K \in OML \land K \in CLat \land K \in AtLat) \land (\forall x \in A \forall y \in A ((x \neq y \to \exists z \in A (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \land \forall z \in B ((\neg x \underset{˙}{\leq} z \land x \underset{˙}{\leq} (z \underset{˙}{\lor} y)) \to y \underset{˙}{\leq} (z \underset{˙}{\lor} x))) \land \exists x \in B \exists y \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}))))$
16	13 14 15	mpbir2an	$⊢ K \in HL$