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 ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( 𝑄𝑅𝑃 ( 𝑄 𝑅 ) ) ↔ 𝑃 𝐶 ( 𝑄 𝑅 ) ) )