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

Metamath Proof Explorer

Theorem hlexch3

Description: A Hilbert lattice has the exchange property. ( atexch analog.) (Contributed by NM, 15-Nov-2011)

Ref Expression
Hypotheses hlexch3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
hlexch3.l ⊢ ≤ = ( le ‘ 𝐾 )
hlexch3.j ⊢ ∨ = ( join ‘ 𝐾 )
hlexch3.m ⊢ ∧ = ( meet ‘ 𝐾 )
hlexch3.z ⊢ 0 = ( 0. ‘ 𝐾 )
hlexch3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion hlexch3 ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 hlexch3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 hlexch3.l ⊢ ≤ = ( le ‘ 𝐾 )
3 hlexch3.j ⊢ ∨ = ( join ‘ 𝐾 )
4 hlexch3.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 hlexch3.z ⊢ 0 = ( 0. ‘ 𝐾 )
6 hlexch3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 hlcvl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
8 1 2 3 4 5 6 cvlexch3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )
9 7 8 syl3an1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )