Theorem cvlexch4N

Description: An atomic covering lattice has the exchange property. Part of Definition 7.8 of MaedaMaeda p. 32. (Contributed by NM, 5-Nov-2012) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cvlexch3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cvlexch3.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cvlexch3.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cvlexch3.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cvlexch3.z	⊢ 0 = ( 0. ‘ 𝐾 )
6		cvlexch3.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7		cvlatl	⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ AtLat )
8	7	adantr	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝐾 ∈ AtLat )
9		simpr1	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑃 ∈ 𝐴 )
10		simpr3	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
11	1 2 4 5 6	atnle	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 0 ) )
12	8 9 10 11	syl3anc	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ¬ 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 0 ) )
13	1 2 3 6	cvlexchb1	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )
14	13	3expia	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ¬ 𝑃 ≤ 𝑋 → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) ) )
15	12 14	sylbird	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑃 ∧ 𝑋 ) = 0 → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) ) )
16	15	3impia	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑄 ) ) )