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 𝐶 ( 𝑃 ∨ 𝑄 ) ↔ 𝑃 = 𝑄 ) )