Metamath Proof Explorer

Theorem atcvr0eq

Description: The covers relation is not transitive. ( atcv0eq analog.) (Contributed by NM, 29-Nov-2011)

Ref Expression
Hypotheses atcvr0eq.j ⊢ ∨ ˙ = join ⁡ K
atcvr0eq.z ⊢ 0 ˙ = 0. ⁡ K
atcvr0eq.c ⊢ C = ⋖ K
atcvr0eq.a ⊢ A = Atoms ⁡ K
Assertion atcvr0eq ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → 0 ˙ C P ∨ ˙ Q ↔ P = Q

Proof

Step Hyp Ref Expression
1 atcvr0eq.j ⊢ ∨ ˙ = join ⁡ K
2 atcvr0eq.z ⊢ 0 ˙ = 0. ⁡ K
3 atcvr0eq.c ⊢ C = ⋖ K
4 atcvr0eq.a ⊢ A = Atoms ⁡ K
5 1 3 4 atcvr1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P C P ∨ ˙ Q
6 2 3 4 atcvr0 ⊢ K ∈ HL ∧ P ∈ A → 0 ˙ C P
7 6 3adant3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → 0 ˙ C P
8 7 biantrurd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P C P ∨ ˙ Q ↔ 0 ˙ C P ∧ P C P ∨ ˙ Q
9 5 8 bitrd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ 0 ˙ C P ∧ P C P ∨ ˙ Q
10 simp1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → K ∈ HL
11 hlop ⊢ K ∈ HL → K ∈ OP
12 11 3ad2ant1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → K ∈ OP
13 eqid ⊢ Base K = Base K
14 13 2 op0cl ⊢ K ∈ OP → 0 ˙ ∈ Base K
15 12 14 syl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → 0 ˙ ∈ Base K
16 13 4 atbase ⊢ P ∈ A → P ∈ Base K
17 16 3ad2ant2 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∈ Base K
18 13 1 4 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
19 13 3 cvrntr ⊢ K ∈ HL ∧ 0 ˙ ∈ Base K ∧ P ∈ Base K ∧ P ∨ ˙ Q ∈ Base K → 0 ˙ C P ∧ P C P ∨ ˙ Q → ¬ 0 ˙ C P ∨ ˙ Q
20 10 15 17 18 19 syl13anc ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → 0 ˙ C P ∧ P C P ∨ ˙ Q → ¬ 0 ˙ C P ∨ ˙ Q
21 9 20 sylbid ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ≠ Q → ¬ 0 ˙ C P ∨ ˙ Q
22 21 necon4ad ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → 0 ˙ C P ∨ ˙ Q → P = Q
23 1 4 hlatjidm ⊢ K ∈ HL ∧ P ∈ A → P ∨ ˙ P = P
24 23 3adant3 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ P = P
25 7 24 breqtrrd ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → 0 ˙ C P ∨ ˙ P
26 oveq2 ⊢ P = Q → P ∨ ˙ P = P ∨ ˙ Q
27 26 breq2d ⊢ P = Q → 0 ˙ C P ∨ ˙ P ↔ 0 ˙ C P ∨ ˙ Q
28 25 27 syl5ibcom ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P = Q → 0 ˙ C P ∨ ˙ Q
29 22 28 impbid ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → 0 ˙ C P ∨ ˙ Q ↔ P = Q