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 ‘ 𝐾 )
atcvr0eq.z 0 = ( 0. ‘ 𝐾 )
atcvr0eq.c 𝐶 = ( ⋖ ‘ 𝐾 )
atcvr0eq.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atcvr0eq ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 0 𝐶 ( 𝑃 𝑄 ) ↔ 𝑃 = 𝑄 ) )

Proof

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