This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlsupr

Description: A Hilbert lattice has the superposition property. Theorem 13.2 in Crawley p. 107. (Contributed by NM, 30-Jan-2012)

Ref Expression
Hypotheses hlsupr.l ⊢ ≤ = ( le ‘ 𝐾 )
hlsupr.j ⊢ ∨ = ( join ‘ 𝐾 )
hlsupr.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion hlsupr ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 hlsupr.l ⊢ ≤ = ( le ‘ 𝐾 )
2 hlsupr.j ⊢ ∨ = ( join ‘ 𝐾 )
3 hlsupr.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
5 4 1 2 3 hlsuprexch ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ≠ 𝑄 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) ∧ ∀ 𝑟 ∈ ( Base ‘ 𝐾 ) ( ( ¬ 𝑃 ≤ 𝑟 ∧ 𝑃 ≤ ( 𝑟 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑟 ∨ 𝑃 ) ) ) )
6 5 simpld ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
7 6 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ) )