ishlat2

Description: The predicate "is a Hilbert lattice". Here we replace K e. CvLat with the weaker K e. AtLat and show the exchange property explicitly. (Contributed by NM, 5-Nov-2012)

	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	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}))))$

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	1 2 4 7	iscvlat	$⊢ K \in CvLat \leftrightarrow (K \in AtLat \land \forall x \in A \forall y \in A \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)))$
10	9	3anbi3i	$⊢ (K \in OML \land K \in CLat \land K \in CvLat) \leftrightarrow (K \in OML \land K \in CLat \land (K \in AtLat \land \forall x \in A \forall y \in A \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))))$
11		anass	$⊢ (((K \in OML \land K \in CLat) \land K \in AtLat) \land \forall x \in A \forall y \in A \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))) \leftrightarrow ((K \in OML \land K \in CLat) \land (K \in AtLat \land \forall x \in A \forall y \in A \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		df-3an	$⊢ (K \in OML \land K \in CLat \land K \in AtLat) \leftrightarrow ((K \in OML \land K \in CLat) \land K \in AtLat)$
13	12	anbi1i	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land \forall x \in A \forall y \in A \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))) \leftrightarrow (((K \in OML \land K \in CLat) \land K \in AtLat) \land \forall x \in A \forall y \in A \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)))$
14		df-3an	$⊢ (K \in OML \land K \in CLat \land (K \in AtLat \land \forall x \in A \forall y \in A \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)))) \leftrightarrow ((K \in OML \land K \in CLat) \land (K \in AtLat \land \forall x \in A \forall y \in A \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))))$
15	11 13 14	3bitr4ri	$⊢ (K \in OML \land K \in CLat \land (K \in AtLat \land \forall x \in A \forall y \in A \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)))) \leftrightarrow ((K \in OML \land K \in CLat \land K \in AtLat) \land \forall x \in A \forall y \in A \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)))$
16	10 15	bitri	$⊢ (K \in OML \land K \in CLat \land K \in CvLat) \leftrightarrow ((K \in OML \land K \in CLat \land K \in AtLat) \land \forall x \in A \forall y \in A \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)))$
17	16	anbi1i	$⊢ ((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 AtLat) \land \forall x \in A \forall y \in A \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 (\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}))))$
18		anass	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land \forall x \in A \forall y \in A \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 (\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 AtLat) \land (\forall x \in A \forall y \in A \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 (\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})))))$
19		anass	$⊢ ((\forall x \in A \forall y \in A \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 \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 \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 (\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}))))$
20		ancom	$⊢ (\forall x \in A \forall y \in A \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 \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 (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 x \in A \forall y \in A \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)))$
21		r19.26-2	$⊢ \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))) \leftrightarrow (\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 x \in A \forall y \in A \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)))$
22	20 21	bitr4i	$⊢ (\forall x \in A \forall y \in A \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 \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 ((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)))$
23	22	anbi1i	$⊢ ((\forall x \in A \forall y \in A \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 \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 ((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})))$
24	19 23	bitr3i	$⊢ (\forall x \in A \forall y \in A \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 (\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 ((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})))$
25	24	anbi2i	$⊢ ((K \in OML \land K \in CLat \land K \in AtLat) \land (\forall x \in A \forall y \in A \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 (\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 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}))))$
26	18 25	bitri	$⊢ (((K \in OML \land K \in CLat \land K \in AtLat) \land \forall x \in A \forall y \in A \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 (\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 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}))))$
27	8 17 26	3bitri	$⊢ 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}))))$

Metamath Proof Explorer

Theorem ishlat2

Proof