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