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 ∧ 𝑃𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → ∃ 𝑟𝐴 ( 𝑟𝑃𝑟𝑄𝑟 ( 𝑃 𝑄 ) ) )