Theorem cvlatcvr2

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

	Ref	Expression
Hypotheses	cvlatcvr1.j	⊢ ∨ = ( join ‘ 𝐾 )
	cvlatcvr1.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	cvlatcvr1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	cvlatcvr2	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ 𝑃 𝐶 ( 𝑄 ∨ 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cvlatcvr1.j	⊢ ∨ = ( join ‘ 𝐾 )
2		cvlatcvr1.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3		cvlatcvr1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4	1 2 3	cvlatcvr1	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑄 ) ) )
5		simp13	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ CvLat )
6		cvllat	⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ Lat )
7	5 6	syl	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ Lat )
8		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9	8 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
10	9	3ad2ant2	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
11	8 3	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
12	11	3ad2ant3	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
13	8 1	latjcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
14	7 10 12 13	syl3anc	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
15	14	breq2d	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 𝐶 ( 𝑃 ∨ 𝑄 ) ↔ 𝑃 𝐶 ( 𝑄 ∨ 𝑃 ) ) )
16	4 15	bitrd	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ 𝑃 𝐶 ( 𝑄 ∨ 𝑃 ) ) )