Theorem cvlatcvr1

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

Proof

Step	Hyp	Ref	Expression
1		cvlatcvr1.j	⊢ ∨ = ( join ‘ 𝐾 )
2		cvlatcvr1.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3		cvlatcvr1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		simp13	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ CvLat )
5		cvlatl	⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ AtLat )
6	4 5	syl	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
7		eqid	⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
8		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
9	7 8 3	atnem0	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ ( 𝑃 ( meet ‘ 𝐾 ) 𝑄 ) = ( 0. ‘ 𝐾 ) ) )
10	6 9	syld3an1	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ ( 𝑃 ( meet ‘ 𝐾 ) 𝑄 ) = ( 0. ‘ 𝐾 ) ) )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	11 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
13	11 1 7 8 2 3	cvlcvrp	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ( meet ‘ 𝐾 ) 𝑄 ) = ( 0. ‘ 𝐾 ) ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑄 ) ) )
14	12 13	syl3an2	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ( 𝑃 ( meet ‘ 𝐾 ) 𝑄 ) = ( 0. ‘ 𝐾 ) ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑄 ) ) )
15	10 14	bitrd	⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑄 ) ) )