Theorem atcvr1

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	atcvr1	⊢ ( ( 𝐾 ∈ 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	cvlatcvr1	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑄 ) ) )
6	4 5	syl3an1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑄 ) ) )