This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )