ishlat1

Description: The predicate "is a Hilbert lattice", which is: is orthomodular ( K e. OML ), complete ( K e. CLat ), atomic and satisfies the exchange (or covering) property ( K e. CvLat ), satisfies the superposition principle, and has a minimum height of 4 (witnessed here by 0, x, y, z, 1). (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	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}))))$

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		fveq2	$⊢ k = K \to Atoms (k) = Atoms (K)$
9	8 7	eqtr4di	$⊢ k = K \to Atoms (k) = A$
10		fveq2	$⊢ k = K \to \leq_{k} = \leq_{K}$
11	10 2	eqtr4di	$⊢ k = K \to \leq_{k} = \underset{˙}{\leq}$
12	11	breqd	$⊢ k = K \to (z \leq_{k} (x join (k) y) \leftrightarrow z \underset{˙}{\leq} (x join (k) y))$
13		fveq2	$⊢ k = K \to join (k) = join (K)$
14	13 4	eqtr4di	$⊢ k = K \to join (k) = \underset{˙}{\lor}$
15	14	oveqd	$⊢ k = K \to x join (k) y = x \underset{˙}{\lor} y$
16	15	breq2d	$⊢ k = K \to (z \underset{˙}{\leq} (x join (k) y) \leftrightarrow z \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
17	12 16	bitrd	$⊢ k = K \to (z \leq_{k} (x join (k) y) \leftrightarrow z \underset{˙}{\leq} (x \underset{˙}{\lor} y))$
18	17	3anbi3d	$⊢ k = K \to ((z \neq x \land z \neq y \land z \leq_{k} (x join (k) y)) \leftrightarrow (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)))$
19	9 18	rexeqbidv	$⊢ k = K \to (\exists z \in Atoms (k) (z \neq x \land z \neq y \land z \leq_{k} (x join (k) y)) \leftrightarrow \exists z \in A (z \neq x \land z \neq y \land z \underset{˙}{\leq} (x \underset{˙}{\lor} y)))$
20	19	imbi2d	$⊢ k = K \to ((x \neq y \to \exists z \in Atoms (k) (z \neq x \land z \neq y \land z \leq_{k} (x join (k) 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))))$
21	9 20	raleqbidv	$⊢ k = K \to (\forall y \in Atoms (k) (x \neq y \to \exists z \in Atoms (k) (z \neq x \land z \neq y \land z \leq_{k} (x join (k) y))) \leftrightarrow \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))))$
22	9 21	raleqbidv	$⊢ k = K \to (\forall x \in Atoms (k) \forall y \in Atoms (k) (x \neq y \to \exists z \in Atoms (k) (z \neq x \land z \neq y \land z \leq_{k} (x join (k) 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))))$
23		fveq2	$⊢ k = K \to {Base}_{k} = {Base}_{K}$
24	23 1	eqtr4di	$⊢ k = K \to {Base}_{k} = B$
25		fveq2	$⊢ k = K \to <_{k} = <_{K}$
26	25 3	eqtr4di	$⊢ k = K \to <_{k} = \underset{˙}{<}$
27	26	breqd	$⊢ k = K \to (0. (k) <_{k} x \leftrightarrow 0. (k) \underset{˙}{<} x)$
28		fveq2	$⊢ k = K \to 0. (k) = 0. (K)$
29	28 5	eqtr4di	$⊢ k = K \to 0. (k) = \underset{˙}{0}$
30	29	breq1d	$⊢ k = K \to (0. (k) \underset{˙}{<} x \leftrightarrow \underset{˙}{0} \underset{˙}{<} x)$
31	27 30	bitrd	$⊢ k = K \to (0. (k) <_{k} x \leftrightarrow \underset{˙}{0} \underset{˙}{<} x)$
32	26	breqd	$⊢ k = K \to (x <_{k} y \leftrightarrow x \underset{˙}{<} y)$
33	31 32	anbi12d	$⊢ k = K \to ((0. (k) <_{k} x \land x <_{k} y) \leftrightarrow (\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y))$
34	26	breqd	$⊢ k = K \to (y <_{k} z \leftrightarrow y \underset{˙}{<} z)$
35	26	breqd	$⊢ k = K \to (z <_{k} 1. (k) \leftrightarrow z \underset{˙}{<} 1. (k))$
36		fveq2	$⊢ k = K \to 1. (k) = 1. (K)$
37	36 6	eqtr4di	$⊢ k = K \to 1. (k) = \underset{˙}{1}$
38	37	breq2d	$⊢ k = K \to (z \underset{˙}{<} 1. (k) \leftrightarrow z \underset{˙}{<} \underset{˙}{1})$
39	35 38	bitrd	$⊢ k = K \to (z <_{k} 1. (k) \leftrightarrow z \underset{˙}{<} \underset{˙}{1})$
40	34 39	anbi12d	$⊢ k = K \to ((y <_{k} z \land z <_{k} 1. (k)) \leftrightarrow (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}))$
41	33 40	anbi12d	$⊢ k = K \to (((0. (k) <_{k} x \land x <_{k} y) \land (y <_{k} z \land z <_{k} 1. (k))) \leftrightarrow ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1})))$
42	24 41	rexeqbidv	$⊢ k = K \to (\exists z \in {Base}_{k} ((0. (k) <_{k} x \land x <_{k} y) \land (y <_{k} z \land z <_{k} 1. (k))) \leftrightarrow \exists z \in B ((\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} y) \land (y \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1})))$
43	24 42	rexeqbidv	$⊢ k = K \to (\exists y \in {Base}_{k} \exists z \in {Base}_{k} ((0. (k) <_{k} x \land x <_{k} y) \land (y <_{k} z \land z <_{k} 1. (k))) \leftrightarrow \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})))$
44	24 43	rexeqbidv	$⊢ k = K \to (\exists x \in {Base}_{k} \exists y \in {Base}_{k} \exists z \in {Base}_{k} ((0. (k) <_{k} x \land x <_{k} y) \land (y <_{k} z \land z <_{k} 1. (k))) \leftrightarrow \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})))$
45	22 44	anbi12d	$⊢ k = K \to ((\forall x \in Atoms (k) \forall y \in Atoms (k) (x \neq y \to \exists z \in Atoms (k) (z \neq x \land z \neq y \land z \leq_{k} (x join (k) y))) \land \exists x \in {Base}_{k} \exists y \in {Base}_{k} \exists z \in {Base}_{k} ((0. (k) <_{k} x \land x <_{k} y) \land (y <_{k} z \land z <_{k} 1. (k)))) \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 \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}))))$
46		df-hlat	$⊢ HL = \{k \in ((OML \cap CLat) \cap CvLat) \| (\forall x \in Atoms (k) \forall y \in Atoms (k) (x \neq y \to \exists z \in Atoms (k) (z \neq x \land z \neq y \land z \leq_{k} (x join (k) y))) \land \exists x \in {Base}_{k} \exists y \in {Base}_{k} \exists z \in {Base}_{k} ((0. (k) <_{k} x \land x <_{k} y) \land (y <_{k} z \land z <_{k} 1. (k))))\}$
47	45 46	elrab2	$⊢ K \in HL \leftrightarrow (K \in ((OML \cap CLat) \cap 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}))))$
48		elin	$⊢ K \in (OML \cap CLat) \leftrightarrow (K \in OML \land K \in CLat)$
49	48	anbi1i	$⊢ (K \in (OML \cap CLat) \land K \in CvLat) \leftrightarrow ((K \in OML \land K \in CLat) \land K \in CvLat)$
50		elin	$⊢ K \in ((OML \cap CLat) \cap CvLat) \leftrightarrow (K \in (OML \cap CLat) \land K \in CvLat)$
51		df-3an	$⊢ (K \in OML \land K \in CLat \land K \in CvLat) \leftrightarrow ((K \in OML \land K \in CLat) \land K \in CvLat)$
52	49 50 51	3bitr4ri	$⊢ (K \in OML \land K \in CLat \land K \in CvLat) \leftrightarrow K \in ((OML \cap CLat) \cap CvLat)$
53	52	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 \cap CLat) \cap 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}))))$
54	47 53	bitr4i	$⊢ 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}))))$

Metamath Proof Explorer

Theorem ishlat1

Proof