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 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )