Metamath Proof Explorer


Theorem cdlemi1

Description: Part of proof of Lemma I of Crawley p. 118. (Contributed by NM, 18-Jun-2013)

Ref Expression
Hypotheses cdlemi.b 𝐵 = ( Base ‘ 𝐾 )
cdlemi.l = ( le ‘ 𝐾 )
cdlemi.j = ( join ‘ 𝐾 )
cdlemi.m = ( meet ‘ 𝐾 )
cdlemi.a 𝐴 = ( Atoms ‘ 𝐾 )
cdlemi.h 𝐻 = ( LHyp ‘ 𝐾 )
cdlemi.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
cdlemi.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
cdlemi.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion cdlemi1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( 𝑃 ( 𝑅𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 cdlemi.b 𝐵 = ( Base ‘ 𝐾 )
2 cdlemi.l = ( le ‘ 𝐾 )
3 cdlemi.j = ( join ‘ 𝐾 )
4 cdlemi.m = ( meet ‘ 𝐾 )
5 cdlemi.a 𝐴 = ( Atoms ‘ 𝐾 )
6 cdlemi.h 𝐻 = ( LHyp ‘ 𝐾 )
7 cdlemi.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8 cdlemi.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
9 cdlemi.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
10 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ HL )
11 10 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ Lat )
12 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
13 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑈𝐸 )
14 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐺𝑇 )
15 6 7 9 tendocl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝐺𝑇 ) → ( 𝑈𝐺 ) ∈ 𝑇 )
16 12 13 14 15 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑈𝐺 ) ∈ 𝑇 )
17 simp3l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑃𝐴 )
18 1 5 atbase ( 𝑃𝐴𝑃𝐵 )
19 17 18 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑃𝐵 )
20 1 6 7 ltrncl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐺 ) ∈ 𝑇𝑃𝐵 ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ∈ 𝐵 )
21 12 16 19 20 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ∈ 𝐵 )
22 1 6 7 8 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐺 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 𝑈𝐺 ) ) ∈ 𝐵 )
23 12 16 22 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑅 ‘ ( 𝑈𝐺 ) ) ∈ 𝐵 )
24 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ ( 𝑅 ‘ ( 𝑈𝐺 ) ) ∈ 𝐵 ) → ( 𝑃 ( 𝑅 ‘ ( 𝑈𝐺 ) ) ) ∈ 𝐵 )
25 11 19 23 24 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( 𝑅 ‘ ( 𝑈𝐺 ) ) ) ∈ 𝐵 )
26 1 6 7 8 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐺𝑇 ) → ( 𝑅𝐺 ) ∈ 𝐵 )
27 12 14 26 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑅𝐺 ) ∈ 𝐵 )
28 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ ( 𝑅𝐺 ) ∈ 𝐵 ) → ( 𝑃 ( 𝑅𝐺 ) ) ∈ 𝐵 )
29 11 19 27 28 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( 𝑅𝐺 ) ) ∈ 𝐵 )
30 1 2 3 latlej2 ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ ( ( 𝑈𝐺 ) ‘ 𝑃 ) ∈ 𝐵 ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) )
31 11 19 21 30 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) )
32 2 3 4 5 6 7 8 trlval2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐺 ) ∈ 𝑇 ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑅 ‘ ( 𝑈𝐺 ) ) = ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) 𝑊 ) )
33 16 32 syld3an2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑅 ‘ ( 𝑈𝐺 ) ) = ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) 𝑊 ) )
34 33 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( 𝑅 ‘ ( 𝑈𝐺 ) ) ) = ( 𝑃 ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) 𝑊 ) ) )
35 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ ( ( 𝑈𝐺 ) ‘ 𝑃 ) ∈ 𝐵 ) → ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ∈ 𝐵 )
36 11 19 21 35 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ∈ 𝐵 )
37 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑊𝐻 )
38 1 6 lhpbase ( 𝑊𝐻𝑊𝐵 )
39 37 38 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑊𝐵 )
40 1 2 3 latlej1 ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ ( ( 𝑈𝐺 ) ‘ 𝑃 ) ∈ 𝐵 ) → 𝑃 ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) )
41 11 19 21 40 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝑃 ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) )
42 1 2 3 4 5 atmod3i1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴 ∧ ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ∈ 𝐵𝑊𝐵 ) ∧ 𝑃 ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ) → ( 𝑃 ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) 𝑊 ) ) = ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ( 𝑃 𝑊 ) ) )
43 10 17 36 39 41 42 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) 𝑊 ) ) = ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ( 𝑃 𝑊 ) ) )
44 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
45 2 3 44 5 6 lhpjat2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 𝑊 ) = ( 1. ‘ 𝐾 ) )
46 45 3adant2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 𝑊 ) = ( 1. ‘ 𝐾 ) )
47 46 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ( 𝑃 𝑊 ) ) = ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ( 1. ‘ 𝐾 ) ) )
48 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
49 10 48 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → 𝐾 ∈ OL )
50 1 4 44 olm11 ( ( 𝐾 ∈ OL ∧ ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ∈ 𝐵 ) → ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ( 1. ‘ 𝐾 ) ) = ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) )
51 49 36 50 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ( 1. ‘ 𝐾 ) ) = ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) )
52 47 51 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) ( 𝑃 𝑊 ) ) = ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) )
53 34 43 52 3eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( 𝑅 ‘ ( 𝑈𝐺 ) ) ) = ( 𝑃 ( ( 𝑈𝐺 ) ‘ 𝑃 ) ) )
54 31 53 breqtrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( 𝑃 ( 𝑅 ‘ ( 𝑈𝐺 ) ) ) )
55 2 6 7 8 9 tendotp ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑈𝐸𝐺𝑇 ) → ( 𝑅 ‘ ( 𝑈𝐺 ) ) ( 𝑅𝐺 ) )
56 12 13 14 55 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑅 ‘ ( 𝑈𝐺 ) ) ( 𝑅𝐺 ) )
57 1 2 3 latjlej2 ( ( 𝐾 ∈ Lat ∧ ( ( 𝑅 ‘ ( 𝑈𝐺 ) ) ∈ 𝐵 ∧ ( 𝑅𝐺 ) ∈ 𝐵𝑃𝐵 ) ) → ( ( 𝑅 ‘ ( 𝑈𝐺 ) ) ( 𝑅𝐺 ) → ( 𝑃 ( 𝑅 ‘ ( 𝑈𝐺 ) ) ) ( 𝑃 ( 𝑅𝐺 ) ) ) )
58 11 23 27 19 57 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑅 ‘ ( 𝑈𝐺 ) ) ( 𝑅𝐺 ) → ( 𝑃 ( 𝑅 ‘ ( 𝑈𝐺 ) ) ) ( 𝑃 ( 𝑅𝐺 ) ) ) )
59 56 58 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( 𝑃 ( 𝑅 ‘ ( 𝑈𝐺 ) ) ) ( 𝑃 ( 𝑅𝐺 ) ) )
60 1 2 11 21 25 29 54 59 lattrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑈𝐸𝐺𝑇 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ) → ( ( 𝑈𝐺 ) ‘ 𝑃 ) ( 𝑃 ( 𝑅𝐺 ) ) )