hlhgt2

Description: A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011)

	Ref	Expression
Hypotheses	hlhgt4.b	$⊢ B = {Base}_{K}$
	hlhgt4.s	$⊢ \underset{˙}{<} = <_{K}$
	hlhgt4.z	$⊢ \underset{˙}{0} = 0. (K)$
	hlhgt4.u	$⊢ \underset{˙}{1} = 1. (K)$
Assertion	hlhgt2	$⊢ K \in HL \to \exists x \in B (\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} \underset{˙}{1})$

Proof

Step	Hyp	Ref	Expression
1		hlhgt4.b	$⊢ B = {Base}_{K}$
2		hlhgt4.s	$⊢ \underset{˙}{<} = <_{K}$
3		hlhgt4.z	$⊢ \underset{˙}{0} = 0. (K)$
4		hlhgt4.u	$⊢ \underset{˙}{1} = 1. (K)$
5	1 2 3 4	hlhgt4	$⊢ K \in HL \to \exists y \in B \exists x \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} y \land y \underset{˙}{<} x) \land (x \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}))$
6		hlpos	$⊢ K \in HL \to K \in Poset$
7	6	ad3antrrr	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to K \in Poset$
8		hlop	$⊢ K \in HL \to K \in OP$
9	8	ad3antrrr	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to K \in OP$
10	1 3	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in B$
11	9 10	syl	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to \underset{˙}{0} \in B$
12		simpllr	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to y \in B$
13		simplr	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to x \in B$
14	1 2	plttr	$⊢ (K \in Poset \land (\underset{˙}{0} \in B \land y \in B \land x \in B)) \to ((\underset{˙}{0} \underset{˙}{<} y \land y \underset{˙}{<} x) \to \underset{˙}{0} \underset{˙}{<} x)$
15	7 11 12 13 14	syl13anc	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to ((\underset{˙}{0} \underset{˙}{<} y \land y \underset{˙}{<} x) \to \underset{˙}{0} \underset{˙}{<} x)$
16		simpr	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to z \in B$
17	1 4	op1cl	$⊢ K \in OP \to \underset{˙}{1} \in B$
18	9 17	syl	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to \underset{˙}{1} \in B$
19	1 2	plttr	$⊢ (K \in Poset \land (x \in B \land z \in B \land \underset{˙}{1} \in B)) \to ((x \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}) \to x \underset{˙}{<} \underset{˙}{1})$
20	7 13 16 18 19	syl13anc	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to ((x \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1}) \to x \underset{˙}{<} \underset{˙}{1})$
21	15 20	anim12d	$⊢ (((K \in HL \land y \in B) \land x \in B) \land z \in B) \to (((\underset{˙}{0} \underset{˙}{<} y \land y \underset{˙}{<} x) \land (x \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1})) \to (\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} \underset{˙}{1}))$
22	21	rexlimdva	$⊢ ((K \in HL \land y \in B) \land x \in B) \to (\exists z \in B ((\underset{˙}{0} \underset{˙}{<} y \land y \underset{˙}{<} x) \land (x \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1})) \to (\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} \underset{˙}{1}))$
23	22	reximdva	$⊢ (K \in HL \land y \in B) \to (\exists x \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} y \land y \underset{˙}{<} x) \land (x \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1})) \to \exists x \in B (\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} \underset{˙}{1}))$
24	23	rexlimdva	$⊢ K \in HL \to (\exists y \in B \exists x \in B \exists z \in B ((\underset{˙}{0} \underset{˙}{<} y \land y \underset{˙}{<} x) \land (x \underset{˙}{<} z \land z \underset{˙}{<} \underset{˙}{1})) \to \exists x \in B (\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} \underset{˙}{1}))$
25	5 24	mpd	$⊢ K \in HL \to \exists x \in B (\underset{˙}{0} \underset{˙}{<} x \land x \underset{˙}{<} \underset{˙}{1})$

Metamath Proof Explorer

Theorem hlhgt2

Proof