Theorem atcvrj1

Description: Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012)

	Ref	Expression
Hypotheses	atcvrj1x.l	⊢ ≤ = ( le ‘ 𝐾 )
	atcvrj1x.j	⊢ ∨ = ( join ‘ 𝐾 )
	atcvrj1x.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
	atcvrj1x.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	atcvrj1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		atcvrj1x.l	⊢ ≤ = ( le ‘ 𝐾 )
2		atcvrj1x.j	⊢ ∨ = ( join ‘ 𝐾 )
3		atcvrj1x.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4		atcvrj1x.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		simp3l	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ≠ 𝑅 )
6		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
7	6	3ad2ant1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝐾 ∈ AtLat )
8		simp21	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝐴 )
9		simp23	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑅 ∈ 𝐴 )
10		eqid	⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
11		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
12	10 11 4	atnem0	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑅 ↔ ( 𝑃 ( meet ‘ 𝐾 ) 𝑅 ) = ( 0. ‘ 𝐾 ) ) )
13	7 8 9 12	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ≠ 𝑅 ↔ ( 𝑃 ( meet ‘ 𝐾 ) 𝑅 ) = ( 0. ‘ 𝐾 ) ) )
14	5 13	mpbid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ( meet ‘ 𝐾 ) 𝑅 ) = ( 0. ‘ 𝐾 ) )
15		simp1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝐾 ∈ HL )
16		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17	16 4	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
18	8 17	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
19	16 2 10 11 3 4	cvrp	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ 𝐴 ) → ( ( 𝑃 ( meet ‘ 𝐾 ) 𝑅 ) = ( 0. ‘ 𝐾 ) ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑅 ) ) )
20	15 18 9 19	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( ( 𝑃 ( meet ‘ 𝐾 ) 𝑅 ) = ( 0. ‘ 𝐾 ) ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑅 ) ) )
21	14 20	mpbid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 𝐶 ( 𝑃 ∨ 𝑅 ) )
22		simp3r	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
23	1 2 4	hlatexchb2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) )
24	23	3adant3r	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) )
25	22 24	mpbid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) )
26	21 25	breqtrd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )