Theorem hl0lt1N

Description: Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hl0lt1.s	⊢ < = ( lt ‘ 𝐾 )
	hl0lt1.z	⊢ 0 = ( 0. ‘ 𝐾 )
	hl0lt1.u	⊢ 1 = ( 1. ‘ 𝐾 )
Assertion	hl0lt1N	⊢ ( 𝐾 ∈ HL → 0 < 1 )

Proof

Step	Hyp	Ref	Expression
1		hl0lt1.s	⊢ < = ( lt ‘ 𝐾 )
2		hl0lt1.z	⊢ 0 = ( 0. ‘ 𝐾 )
3		hl0lt1.u	⊢ 1 = ( 1. ‘ 𝐾 )
4		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5	4 1 2 3	hlhgt2	⊢ ( 𝐾 ∈ HL → ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 0 < 𝑥 ∧ 𝑥 < 1 ) )
6		hlpos	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
7	6	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ Poset )
8		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
9	8	adantr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ OP )
10	4 2	op0cl	⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
11	9 10	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 0 ∈ ( Base ‘ 𝐾 ) )
12		simpr	⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
13	4 3	op1cl	⊢ ( 𝐾 ∈ OP → 1 ∈ ( Base ‘ 𝐾 ) )
14	9 13	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 1 ∈ ( Base ‘ 𝐾 ) )
15	4 1	plttr	⊢ ( ( 𝐾 ∈ Poset ∧ ( 0 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 1 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 0 < 𝑥 ∧ 𝑥 < 1 ) → 0 < 1 ) )
16	7 11 12 14 15	syl13anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0 < 𝑥 ∧ 𝑥 < 1 ) → 0 < 1 ) )
17	16	rexlimdva	⊢ ( 𝐾 ∈ HL → ( ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 0 < 𝑥 ∧ 𝑥 < 1 ) → 0 < 1 ) )
18	5 17	mpd	⊢ ( 𝐾 ∈ HL → 0 < 1 )