Metamath Proof Explorer


Theorem hlhgt2

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

Ref Expression
Hypotheses hlhgt4.b B=BaseK
hlhgt4.s <˙=<K
hlhgt4.z 0˙=0.K
hlhgt4.u 1˙=1.K
Assertion hlhgt2 KHLxB0˙<˙xx<˙1˙

Proof

Step Hyp Ref Expression
1 hlhgt4.b B=BaseK
2 hlhgt4.s <˙=<K
3 hlhgt4.z 0˙=0.K
4 hlhgt4.u 1˙=1.K
5 1 2 3 4 hlhgt4 KHLyBxBzB0˙<˙yy<˙xx<˙zz<˙1˙
6 hlpos KHLKPoset
7 6 ad3antrrr KHLyBxBzBKPoset
8 hlop KHLKOP
9 8 ad3antrrr KHLyBxBzBKOP
10 1 3 op0cl KOP0˙B
11 9 10 syl KHLyBxBzB0˙B
12 simpllr KHLyBxBzByB
13 simplr KHLyBxBzBxB
14 1 2 plttr KPoset0˙ByBxB0˙<˙yy<˙x0˙<˙x
15 7 11 12 13 14 syl13anc KHLyBxBzB0˙<˙yy<˙x0˙<˙x
16 simpr KHLyBxBzBzB
17 1 4 op1cl KOP1˙B
18 9 17 syl KHLyBxBzB1˙B
19 1 2 plttr KPosetxBzB1˙Bx<˙zz<˙1˙x<˙1˙
20 7 13 16 18 19 syl13anc KHLyBxBzBx<˙zz<˙1˙x<˙1˙
21 15 20 anim12d KHLyBxBzB0˙<˙yy<˙xx<˙zz<˙1˙0˙<˙xx<˙1˙
22 21 rexlimdva KHLyBxBzB0˙<˙yy<˙xx<˙zz<˙1˙0˙<˙xx<˙1˙
23 22 reximdva KHLyBxBzB0˙<˙yy<˙xx<˙zz<˙1˙xB0˙<˙xx<˙1˙
24 23 rexlimdva KHLyBxBzB0˙<˙yy<˙xx<˙zz<˙1˙xB0˙<˙xx<˙1˙
25 5 24 mpd KHLxB0˙<˙xx<˙1˙