Metamath Proof Explorer


Theorem atcvr2

Description: An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012)

Ref Expression
Hypotheses atcvr1.j = ( join ‘ 𝐾 )
atcvr1.c 𝐶 = ( ⋖ ‘ 𝐾 )
atcvr1.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atcvr2 ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃𝑄𝑃 𝐶 ( 𝑄 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 atcvr1.j = ( join ‘ 𝐾 )
2 atcvr1.c 𝐶 = ( ⋖ ‘ 𝐾 )
3 atcvr1.a 𝐴 = ( Atoms ‘ 𝐾 )
4 hlomcmcv ( 𝐾 ∈ HL → ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) )
5 1 2 3 cvlatcvr2 ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃𝑄𝑃 𝐶 ( 𝑄 𝑃 ) ) )
6 4 5 syl3an1 ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃𝑄𝑃 𝐶 ( 𝑄 𝑃 ) ) )