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

Metamath Proof Explorer

Theorem cvlatexch1

Description: Atom exchange property. (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlatexch.l ⊢ ≤ = ( le ‘ 𝐾 )
cvlatexch.j ⊢ ∨ = ( join ‘ 𝐾 )
cvlatexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvlatexch1 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑅 ∨ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 cvlatexch.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cvlatexch.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cvlatexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 1 2 3 cvlatexchb1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ↔ ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑄 ) ) )
5 cvllat ⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ Lat )
6 5 3ad2ant1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → 𝐾 ∈ Lat )
7 simp23 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → 𝑅 ∈ 𝐴 )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
10 7 9 syl ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
11 simp22 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → 𝑄 ∈ 𝐴 )
12 8 3 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
13 11 12 syl ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
14 8 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → 𝑄 ≤ ( 𝑅 ∨ 𝑄 ) )
15 6 10 13 14 syl3anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → 𝑄 ≤ ( 𝑅 ∨ 𝑄 ) )
16 breq2 ⊢ ( ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑄 ) → ( 𝑄 ≤ ( 𝑅 ∨ 𝑃 ) ↔ 𝑄 ≤ ( 𝑅 ∨ 𝑄 ) ) )
17 15 16 syl5ibrcom ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑅 ∨ 𝑃 ) ) )
18 4 17 sylbid ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑅 ∨ 𝑃 ) ) )