Metamath Proof Explorer


Theorem cdleme0e

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 13-Jun-2012)

Ref Expression
Hypotheses cdleme0.l = ( le ‘ 𝐾 )
cdleme0.j = ( join ‘ 𝐾 )
cdleme0.m = ( meet ‘ 𝐾 )
cdleme0.a 𝐴 = ( Atoms ‘ 𝐾 )
cdleme0.h 𝐻 = ( LHyp ‘ 𝐾 )
cdleme0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
cdleme0c.3 𝑉 = ( ( 𝑃 𝑅 ) 𝑊 )
Assertion cdleme0e ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑈𝑉 )

Proof

Step Hyp Ref Expression
1 cdleme0.l = ( le ‘ 𝐾 )
2 cdleme0.j = ( join ‘ 𝐾 )
3 cdleme0.m = ( meet ‘ 𝐾 )
4 cdleme0.a 𝐴 = ( Atoms ‘ 𝐾 )
5 cdleme0.h 𝐻 = ( LHyp ‘ 𝐾 )
6 cdleme0.u 𝑈 = ( ( 𝑃 𝑄 ) 𝑊 )
7 cdleme0c.3 𝑉 = ( ( 𝑃 𝑅 ) 𝑊 )
8 6 7 oveq12i ( 𝑈 𝑉 ) = ( ( ( 𝑃 𝑄 ) 𝑊 ) ( ( 𝑃 𝑅 ) 𝑊 ) )
9 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ HL )
10 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
11 9 10 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ OL )
12 simp21l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑃𝐴 )
13 simp22 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑄𝐴 )
14 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15 14 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
16 9 12 13 15 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
17 simp23l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑅𝐴 )
18 14 2 4 hlatjcl ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴 ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
19 9 12 17 18 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
20 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑊𝐻 )
21 14 5 lhpbase ( 𝑊𝐻𝑊 ∈ ( Base ‘ 𝐾 ) )
22 20 21 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
23 14 3 latmmdir ( ( 𝐾 ∈ OL ∧ ( ( 𝑃 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 𝑅 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑃 𝑅 ) ) 𝑊 ) = ( ( ( 𝑃 𝑄 ) 𝑊 ) ( ( 𝑃 𝑅 ) 𝑊 ) ) )
24 11 16 19 22 23 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑃 𝑅 ) ) 𝑊 ) = ( ( ( 𝑃 𝑄 ) 𝑊 ) ( ( 𝑃 𝑅 ) 𝑊 ) ) )
25 9 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ Lat )
26 14 4 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
27 17 26 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
28 14 4 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
29 12 28 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
30 14 4 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
31 13 30 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
32 simp3r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
33 14 1 2 latnlej1r ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅𝑄 )
34 33 necomd ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑄𝑅 )
35 25 27 29 31 32 34 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑄𝑅 )
36 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) )
37 1 2 4 hlatcon3 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ¬ 𝑃 ( 𝑄 𝑅 ) )
38 9 12 13 17 36 37 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ¬ 𝑃 ( 𝑄 𝑅 ) )
39 1 2 3 4 2llnma2 ( ( 𝐾 ∈ HL ∧ ( 𝑄𝐴𝑅𝐴𝑃𝐴 ) ∧ ( 𝑄𝑅 ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑃 𝑅 ) ) = 𝑃 )
40 9 13 17 12 35 38 39 syl132anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( 𝑃 𝑄 ) ( 𝑃 𝑅 ) ) = 𝑃 )
41 40 oveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑃 𝑄 ) ( 𝑃 𝑅 ) ) 𝑊 ) = ( 𝑃 𝑊 ) )
42 24 41 eqtr3d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( ( ( 𝑃 𝑄 ) 𝑊 ) ( ( 𝑃 𝑅 ) 𝑊 ) ) = ( 𝑃 𝑊 ) )
43 8 42 syl5eq ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑈 𝑉 ) = ( 𝑃 𝑊 ) )
44 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
45 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
46 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
47 1 3 46 4 5 lhpmat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 𝑊 ) = ( 0. ‘ 𝐾 ) )
48 44 45 47 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑃 𝑊 ) = ( 0. ‘ 𝐾 ) )
49 43 48 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑈 𝑉 ) = ( 0. ‘ 𝐾 ) )
50 hlatl ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
51 9 50 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝐾 ∈ AtLat )
52 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑃𝑄 )
53 1 2 3 4 5 6 lhpat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑄𝐴𝑃𝑄 ) ) → 𝑈𝐴 )
54 44 45 13 52 53 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑈𝐴 )
55 14 1 2 latnlej1l ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅𝑃 )
56 55 necomd ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑃𝑅 )
57 25 27 29 31 32 56 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑃𝑅 )
58 1 2 3 4 5 7 lhpat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑅𝐴𝑃𝑅 ) ) → 𝑉𝐴 )
59 44 45 17 57 58 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑉𝐴 )
60 3 46 4 atnem0 ( ( 𝐾 ∈ AtLat ∧ 𝑈𝐴𝑉𝐴 ) → ( 𝑈𝑉 ↔ ( 𝑈 𝑉 ) = ( 0. ‘ 𝐾 ) ) )
61 51 54 59 60 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → ( 𝑈𝑉 ↔ ( 𝑈 𝑉 ) = ( 0. ‘ 𝐾 ) ) )
62 49 61 mpbird ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ 𝑄𝐴 ∧ ( 𝑅𝐴 ∧ ¬ 𝑅 𝑊 ) ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) ) → 𝑈𝑉 )