ishlat3N

Description: The predicate "is a Hilbert lattice". Note that the superposition principle is expressed in the compact form E. z e. A ( x .\/ z ) = ( y .\/ z ) . The exchange property and atomicity are provided by K e. CvLat , and "minimum height 4" is shown explicitly. (Contributed by NM, 8-Nov-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ishlat.b	$⊢ B = {Base}_{K}$
	ishlat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	ishlat.s	$⊢ \underset{˙}{<} = <_{K}$
	ishlat.j	$⊢ \underset{˙}{\lor} = join (K)$
	ishlat.z	$⊢ \underset{˙}{0} = 0. (K)$
	ishlat.u	$⊢ \underset{˙}{1} = 1. (K)$
	ishlat.a	$⊢ A = Atoms (K)$
Assertion	ishlat3N	$⊢ K \in HL \leftrightarrow ((K \in OML \land K \in CLat \land K \in CvLat) \land (\forall x \in A \forall y \in A \exists z \in A x \underset{˙}{\lor} z = y \underset{˙}{\lor} z \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}))))$

Proof

Step	Hyp	Ref	Expression
1		ishlat.b	$⊢ B = {Base}_{K}$
2		ishlat.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		ishlat.s	$⊢ \underset{˙}{<} = <_{K}$
4		ishlat.j	$⊢ \underset{˙}{\lor} = join (K)$
5		ishlat.z	$⊢ \underset{˙}{0} = 0. (K)$
6		ishlat.u	$⊢ \underset{˙}{1} = 1. (K)$
7		ishlat.a	$⊢ A = Atoms (K)$
8	1 2 3 4 5 6 7	ishlat1	$⊢ K \in HL \leftrightarrow ((K \in OML \land K \in CLat \land K \in CvLat) \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 \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}))))$
9		simpll3	$⊢ (((K \in OML \land K \in CLat \land K \in CvLat) \land (x \in A \land y \in A)) \land z \in A) \to K \in CvLat$
10		simplrl	$⊢ (((K \in OML \land K \in CLat \land K \in CvLat) \land (x \in A \land y \in A)) \land z \in A) \to x \in A$
11		simplrr	$⊢ (((K \in OML \land K \in CLat \land K \in CvLat) \land (x \in A \land y \in A)) \land z \in A) \to y \in A$
12		simpr	$⊢ (((K \in OML \land K \in CLat \land K \in CvLat) \land (x \in A \land y \in A)) \land z \in A) \to z \in A$
13	7 2 4	cvlsupr3	$⊢ (K \in CvLat \land (x \in A \land y \in A \land z \in A)) \to (x \underset{˙}{\lor} z = y \underset{˙}{\lor} z \leftrightarrow (x \neq y \to (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))))$
14	9 10 11 12 13	syl13anc	$⊢ (((K \in OML \land K \in CLat \land K \in CvLat) \land (x \in A \land y \in A)) \land z \in A) \to (x \underset{˙}{\lor} z = y \underset{˙}{\lor} z \leftrightarrow (x \neq y \to (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))))$
15	14	rexbidva	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land (x \in A \land y \in A)) \to (\exists z \in A x \underset{˙}{\lor} z = y \underset{˙}{\lor} z \leftrightarrow \exists z \in A (x \neq y \to (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))))$
16		ne0i	$⊢ x \in A \to A \neq \emptyset$
17	16	ad2antrl	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land (x \in A \land y \in A)) \to A \neq \emptyset$
18		r19.37zv	$⊢ A \neq \emptyset \to (\exists z \in A (x \neq y \to (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \leftrightarrow (x \neq y \to \exists z \in A (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))))$
19	17 18	syl	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land (x \in A \land y \in A)) \to (\exists z \in A (x \neq y \to (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \leftrightarrow (x \neq y \to \exists z \in A (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))))$
20	15 19	bitr2d	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \land (x \in A \land y \in A)) \to ((x \neq y \to \exists z \in A (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y))) \leftrightarrow \exists z \in A x \underset{˙}{\lor} z = y \underset{˙}{\lor} z)$
21	20	2ralbidva	$⊢ (K \in OML \land K \in CLat \land K \in CvLat) \to (\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))) \leftrightarrow \forall x \in A \forall y \in A \exists z \in A x \underset{˙}{\lor} z = y \underset{˙}{\lor} z)$
22	21	anbi1d	$⊢ (K \in OML \land K \in CLat \land K \in CvLat) \to ((\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 \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}))) \leftrightarrow (\forall x \in A \forall y \in A \exists z \in A x \underset{˙}{\lor} z = y \underset{˙}{\lor} z \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}))))$
23	22	pm5.32i	$⊢ ((K \in OML \land K \in CLat \land K \in CvLat) \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 \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})))) \leftrightarrow ((K \in OML \land K \in CLat \land K \in CvLat) \land (\forall x \in A \forall y \in A \exists z \in A x \underset{˙}{\lor} z = y \underset{˙}{\lor} z \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}))))$
24	8 23	bitri	$⊢ K \in HL \leftrightarrow ((K \in OML \land K \in CLat \land K \in CvLat) \land (\forall x \in A \forall y \in A \exists z \in A x \underset{˙}{\lor} z = y \underset{˙}{\lor} z \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}))))$

Metamath Proof Explorer

Theorem ishlat3N

Proof