Metamath Proof Explorer

Theorem atcvrneN

Description: Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses atcvrne.j ⊢ ∨ ˙ = join ⁡ K
atcvrne.c ⊢ C = ⋖ K
atcvrne.a ⊢ A = Atoms ⁡ K
Assertion atcvrneN ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → Q ≠ R

Proof

Step Hyp Ref Expression
1 atcvrne.j ⊢ ∨ ˙ = join ⁡ K
2 atcvrne.c ⊢ C = ⋖ K
3 atcvrne.a ⊢ A = Atoms ⁡ K
4 hlatl ⊢ K ∈ HL → K ∈ AtLat
5 4 3ad2ant1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → K ∈ AtLat
6 simp21 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → P ∈ A
7 eqid ⊢ 0. ⁡ K = 0. ⁡ K
8 7 3 atn0 ⊢ K ∈ AtLat ∧ P ∈ A → P ≠ 0. ⁡ K
9 5 6 8 syl2anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → P ≠ 0. ⁡ K
10 simp1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → K ∈ HL
11 eqid ⊢ Base K = Base K
12 11 3 atbase ⊢ P ∈ A → P ∈ Base K
13 6 12 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → P ∈ Base K
14 simp22 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → Q ∈ A
15 simp23 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → R ∈ A
16 simp3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → P C Q ∨ ˙ R
17 11 1 7 2 3 atcvrj0 ⊢ K ∈ HL ∧ P ∈ Base K ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → P = 0. ⁡ K ↔ Q = R
18 10 13 14 15 16 17 syl131anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → P = 0. ⁡ K ↔ Q = R
19 18 necon3bid ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → P ≠ 0. ⁡ K ↔ Q ≠ R
20 9 19 mpbid ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ P C Q ∨ ˙ R → Q ≠ R