Metamath Proof Explorer


Theorem cdlemd3

Description: Part of proof of Lemma D in Crawley p. 113. The R =/= P requirement is not mentioned in their proof. (Contributed by NM, 29-May-2012)

Ref Expression
Hypotheses cdlemd3.l = ( le ‘ 𝐾 )
cdlemd3.j = ( join ‘ 𝐾 )
cdlemd3.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemd3.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion cdlemd3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑅 ( 𝑃 𝑆 ) )

Proof

Step Hyp Ref Expression
1 cdlemd3.l = ( le ‘ 𝐾 )
2 cdlemd3.j = ( join ‘ 𝐾 )
3 cdlemd3.a 𝐴 = ( Atoms ‘ 𝐾 )
4 cdlemd3.h 𝐻 = ( LHyp ‘ 𝐾 )
5 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑆 ( 𝑃 𝑄 ) )
6 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
7 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅𝐴 )
8 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆𝐴 )
9 simp21l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
10 simp233 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅𝑃 )
11 1 2 3 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( 𝑅𝐴𝑆𝐴𝑃𝐴 ) ∧ 𝑅𝑃 ) → ( 𝑅 ( 𝑃 𝑆 ) → 𝑆 ( 𝑃 𝑅 ) ) )
12 6 7 8 9 10 11 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑅 ( 𝑃 𝑆 ) → 𝑆 ( 𝑃 𝑅 ) ) )
13 simp22l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
14 1 2 3 hlatlej1 ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → 𝑃 ( 𝑃 𝑄 ) )
15 6 9 13 14 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃 ( 𝑃 𝑄 ) )
16 simp232 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅 ( 𝑃 𝑄 ) )
17 6 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ Lat )
18 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
19 18 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
20 9 19 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
21 18 3 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
22 7 21 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
23 18 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
24 13 23 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
25 18 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
26 17 20 24 25 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
27 18 1 2 latjle12 ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ↔ ( 𝑃 𝑅 ) ( 𝑃 𝑄 ) ) )
28 17 20 22 26 27 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 ( 𝑃 𝑄 ) ∧ 𝑅 ( 𝑃 𝑄 ) ) ↔ ( 𝑃 𝑅 ) ( 𝑃 𝑄 ) ) )
29 15 16 28 mpbi2and ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑅 ) ( 𝑃 𝑄 ) )
30 18 3 atbase ( 𝑆𝐴𝑆 ∈ ( Base ‘ 𝐾 ) )
31 8 30 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
32 18 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
33 17 20 22 32 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
34 18 1 lattr ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑆 ( 𝑃 𝑅 ) ∧ ( 𝑃 𝑅 ) ( 𝑃 𝑄 ) ) → 𝑆 ( 𝑃 𝑄 ) ) )
35 17 31 33 26 34 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( ( 𝑆 ( 𝑃 𝑅 ) ∧ ( 𝑃 𝑅 ) ( 𝑃 𝑄 ) ) → 𝑆 ( 𝑃 𝑄 ) ) )
36 29 35 mpan2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑆 ( 𝑃 𝑅 ) → 𝑆 ( 𝑃 𝑄 ) ) )
37 12 36 syld ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ( 𝑅 ( 𝑃 𝑆 ) → 𝑆 ( 𝑃 𝑄 ) ) )
38 5 37 mtod ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴 ∧ ¬ 𝑄 𝑊 ) ∧ ( 𝑃𝑄𝑅 ( 𝑃 𝑄 ) ∧ 𝑅𝑃 ) ) ∧ ( 𝑅𝐴𝑆𝐴 ∧ ¬ 𝑆 ( 𝑃 𝑄 ) ) ) → ¬ 𝑅 ( 𝑃 𝑆 ) )