Metamath Proof Explorer

Theorem atcvrj2b

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

Proof

Step Hyp Ref Expression
1 atcvrj1x.l ⊢ ≤ = ( le ‘ 𝐾 )
2 atcvrj1x.j ⊢ ∨ = ( join ‘ 𝐾 )
3 atcvrj1x.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4 atcvrj1x.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simpl3l ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 = 𝑅 ) → 𝑄 ≠ 𝑅 )
6 5 necomd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 = 𝑅 ) → 𝑅 ≠ 𝑄 )
7 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 = 𝑅 ) → 𝐾 ∈ HL )
8 simpl23 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 = 𝑅 ) → 𝑅 ∈ 𝐴 )
9 simpl22 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 = 𝑅 ) → 𝑄 ∈ 𝐴 )
10 2 3 4 atcvr2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑅 ≠ 𝑄 ↔ 𝑅 𝐶 ( 𝑄 ∨ 𝑅 ) ) )
11 7 8 9 10 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 = 𝑅 ) → ( 𝑅 ≠ 𝑄 ↔ 𝑅 𝐶 ( 𝑄 ∨ 𝑅 ) ) )
12 6 11 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 = 𝑅 ) → 𝑅 𝐶 ( 𝑄 ∨ 𝑅 ) )
13 breq1 ⊢ ( 𝑃 = 𝑅 → ( 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ↔ 𝑅 𝐶 ( 𝑄 ∨ 𝑅 ) ) )
14 13 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 = 𝑅 ) → ( 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ↔ 𝑅 𝐶 ( 𝑄 ∨ 𝑅 ) ) )
15 12 14 mpbird ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 = 𝑅 ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )
16 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 ≠ 𝑅 ) → 𝐾 ∈ HL )
17 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) )
18 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 ≠ 𝑅 ) → 𝑃 ≠ 𝑅 )
19 simpl3r ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 ≠ 𝑅 ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
20 1 2 3 4 atcvrj1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )
21 16 17 18 19 20 syl112anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ∧ 𝑃 ≠ 𝑅 ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )
22 15 21 pm2.61dane ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )
23 22 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) )
24 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
25 24 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ AtLat )
26 simplr1 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ 𝐴 )
27 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
28 27 4 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ≠ ( 0. ‘ 𝐾 ) )
29 25 26 28 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ≠ ( 0. ‘ 𝐾 ) )
30 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ HL )
31 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
32 31 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
33 26 32 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
34 simplr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ 𝐴 )
35 simplr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ 𝐴 )
36 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) )
37 31 2 27 3 4 atcvrj0 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑃 = ( 0. ‘ 𝐾 ) ↔ 𝑄 = 𝑅 ) )
38 30 33 34 35 36 37 syl131anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑃 = ( 0. ‘ 𝐾 ) ↔ 𝑄 = 𝑅 ) )
39 38 necon3bid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑃 ≠ ( 0. ‘ 𝐾 ) ↔ 𝑄 ≠ 𝑅 ) )
40 29 39 mpbid ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ≠ 𝑅 )
41 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
42 41 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝐾 ∈ Lat )
43 31 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
44 34 43 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
45 31 4 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
46 35 45 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
47 31 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
48 42 44 46 47 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
49 30 33 48 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) )
50 31 1 3 cvrle ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
51 49 50 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) )
52 40 51 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) → ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) )
53 52 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) → ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) )
54 23 53 impbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑄 ≠ 𝑅 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ↔ 𝑃 𝐶 ( 𝑄 ∨ 𝑅 ) ) )