Metamath Proof Explorer

Theorem cvlatcvr1

Description: An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlatcvr1.j ⊢ ∨ ˙ = join ⁡ K
cvlatcvr1.c ⊢ C = ⋖ K
cvlatcvr1.a ⊢ A = Atoms ⁡ K
Assertion cvlatcvr1 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P C P ∨ ˙ Q

Proof

Step Hyp Ref Expression
1 cvlatcvr1.j ⊢ ∨ ˙ = join ⁡ K
2 cvlatcvr1.c ⊢ C = ⋖ K
3 cvlatcvr1.a ⊢ A = Atoms ⁡ K
4 simp13 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → K ∈ CvLat
5 cvlatl ⊢ K ∈ CvLat → K ∈ AtLat
6 4 5 syl ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → K ∈ AtLat
7 eqid ⊢ meet ⁡ K = meet ⁡ K
8 eqid ⊢ 0. ⁡ K = 0. ⁡ K
9 7 8 3 atnem0 ⊢ K ∈ AtLat ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P meet ⁡ K Q = 0. ⁡ K
10 6 9 syld3an1 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P meet ⁡ K Q = 0. ⁡ K
11 eqid ⊢ Base K = Base K
12 11 3 atbase ⊢ P ∈ A → P ∈ Base K
13 11 1 7 8 2 3 cvlcvrp ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ Base K ∧ Q ∈ A → P meet ⁡ K Q = 0. ⁡ K ↔ P C P ∨ ˙ Q
14 12 13 syl3an2 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P meet ⁡ K Q = 0. ⁡ K ↔ P C P ∨ ˙ Q
15 10 14 bitrd ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P C P ∨ ˙ Q