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 𝐵 = ( Base ‘ 𝐾 )
hlhgt4.s < = ( lt ‘ 𝐾 )
hlhgt4.z 0 = ( 0. ‘ 𝐾 )
hlhgt4.u 1 = ( 1. ‘ 𝐾 )
Assertion hlhgt2 ( 𝐾 ∈ HL → ∃ 𝑥𝐵 ( 0 < 𝑥𝑥 < 1 ) )

Proof

Step Hyp Ref Expression
1 hlhgt4.b 𝐵 = ( Base ‘ 𝐾 )
2 hlhgt4.s < = ( lt ‘ 𝐾 )
3 hlhgt4.z 0 = ( 0. ‘ 𝐾 )
4 hlhgt4.u 1 = ( 1. ‘ 𝐾 )
5 1 2 3 4 hlhgt4 ( 𝐾 ∈ HL → ∃ 𝑦𝐵𝑥𝐵𝑧𝐵 ( ( 0 < 𝑦𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧𝑧 < 1 ) ) )
6 hlpos ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
7 6 ad3antrrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → 𝐾 ∈ Poset )
8 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
9 8 ad3antrrr ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → 𝐾 ∈ OP )
10 1 3 op0cl ( 𝐾 ∈ OP → 0𝐵 )
11 9 10 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → 0𝐵 )
12 simpllr ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → 𝑦𝐵 )
13 simplr ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → 𝑥𝐵 )
14 1 2 plttr ( ( 𝐾 ∈ Poset ∧ ( 0𝐵𝑦𝐵𝑥𝐵 ) ) → ( ( 0 < 𝑦𝑦 < 𝑥 ) → 0 < 𝑥 ) )
15 7 11 12 13 14 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → ( ( 0 < 𝑦𝑦 < 𝑥 ) → 0 < 𝑥 ) )
16 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → 𝑧𝐵 )
17 1 4 op1cl ( 𝐾 ∈ OP → 1𝐵 )
18 9 17 syl ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → 1𝐵 )
19 1 2 plttr ( ( 𝐾 ∈ Poset ∧ ( 𝑥𝐵𝑧𝐵1𝐵 ) ) → ( ( 𝑥 < 𝑧𝑧 < 1 ) → 𝑥 < 1 ) )
20 7 13 16 18 19 syl13anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → ( ( 𝑥 < 𝑧𝑧 < 1 ) → 𝑥 < 1 ) )
21 15 20 anim12d ( ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) ∧ 𝑧𝐵 ) → ( ( ( 0 < 𝑦𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧𝑧 < 1 ) ) → ( 0 < 𝑥𝑥 < 1 ) ) )
22 21 rexlimdva ( ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) ∧ 𝑥𝐵 ) → ( ∃ 𝑧𝐵 ( ( 0 < 𝑦𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧𝑧 < 1 ) ) → ( 0 < 𝑥𝑥 < 1 ) ) )
23 22 reximdva ( ( 𝐾 ∈ HL ∧ 𝑦𝐵 ) → ( ∃ 𝑥𝐵𝑧𝐵 ( ( 0 < 𝑦𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧𝑧 < 1 ) ) → ∃ 𝑥𝐵 ( 0 < 𝑥𝑥 < 1 ) ) )
24 23 rexlimdva ( 𝐾 ∈ HL → ( ∃ 𝑦𝐵𝑥𝐵𝑧𝐵 ( ( 0 < 𝑦𝑦 < 𝑥 ) ∧ ( 𝑥 < 𝑧𝑧 < 1 ) ) → ∃ 𝑥𝐵 ( 0 < 𝑥𝑥 < 1 ) ) )
25 5 24 mpd ( 𝐾 ∈ HL → ∃ 𝑥𝐵 ( 0 < 𝑥𝑥 < 1 ) )