Metamath Proof Explorer

Theorem dia2dimlem2

Description: Lemma for dia2dim . Define a translation G whose trace is atom U . Part of proof of Lemma M in Crawley p. 121 line 4. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia2dimlem2.l ⊢ ≤ = ( le ‘ 𝐾 )
dia2dimlem2.j ⊢ ∨ = ( join ‘ 𝐾 )
dia2dimlem2.m ⊢ ∧ = ( meet ‘ 𝐾 )
dia2dimlem2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
dia2dimlem2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dia2dimlem2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem2.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dia2dimlem2.q ⊢ 𝑄 = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
dia2dimlem2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dia2dimlem2.u ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
dia2dimlem2.v ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
dia2dimlem2.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
dia2dimlem2.f ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) )
dia2dimlem2.rf ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
dia2dimlem2.rv ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
dia2dimlem2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑇 )
dia2dimlem2.gv ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑃 ) = 𝑄 )
Assertion dia2dimlem2 ( 𝜑 → ( 𝑅 ‘ 𝐺 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 dia2dimlem2.l ⊢ ≤ = ( le ‘ 𝐾 )
2 dia2dimlem2.j ⊢ ∨ = ( join ‘ 𝐾 )
3 dia2dimlem2.m ⊢ ∧ = ( meet ‘ 𝐾 )
4 dia2dimlem2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 dia2dimlem2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 dia2dimlem2.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7 dia2dimlem2.r ⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8 dia2dimlem2.q ⊢ 𝑄 = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
9 dia2dimlem2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 dia2dimlem2.u ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
11 dia2dimlem2.v ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
12 dia2dimlem2.p ⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
13 dia2dimlem2.f ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) )
14 dia2dimlem2.rf ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
15 dia2dimlem2.rv ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
16 dia2dimlem2.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑇 )
17 dia2dimlem2.gv ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑃 ) = 𝑄 )
18 9 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
19 18 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
20 12 simpld ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 21 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
23 20 22 syl ⊢ ( 𝜑 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
24 10 simpld ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
25 21 4 atbase ⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
26 24 25 syl ⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
27 21 1 2 latlej2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ) → 𝑈 ≤ ( 𝑃 ∨ 𝑈 ) )
28 19 23 26 27 syl3anc ⊢ ( 𝜑 → 𝑈 ≤ ( 𝑃 ∨ 𝑈 ) )
29 21 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
30 18 20 24 29 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) )
31 21 1 3 latleeqm2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑈 ≤ ( 𝑃 ∨ 𝑈 ) ↔ ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑈 ) = 𝑈 ) )
32 19 26 30 31 syl3anc ⊢ ( 𝜑 → ( 𝑈 ≤ ( 𝑃 ∨ 𝑈 ) ↔ ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑈 ) = 𝑈 ) )
33 28 32 mpbid ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑈 ) = 𝑈 )
34 1 4 5 6 7 trlat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
35 9 12 13 34 syl3anc ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 )
36 11 simpld ⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
37 1 2 4 hlatexch2 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) → ( ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) → 𝑈 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑉 ) ) )
38 18 35 24 36 15 37 syl131anc ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) → 𝑈 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑉 ) ) )
39 14 38 mpd ⊢ ( 𝜑 → 𝑈 ≤ ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑉 ) )
40 13 simpld ⊢ ( 𝜑 → 𝐹 ∈ 𝑇 )
41 1 2 3 4 5 6 7 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) )
42 9 40 12 41 syl3anc ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) = ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) )
43 42 oveq1d ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑉 ) = ( ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ 𝑉 ) )
44 1 4 5 6 ltrnel ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
45 9 40 12 44 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ ¬ ( 𝐹 ‘ 𝑃 ) ≤ 𝑊 ) )
46 45 simpld ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 )
47 21 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ) → ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
48 18 20 46 47 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) )
49 9 simprd ⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
50 21 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
51 49 50 syl ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
52 11 simprd ⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
53 21 1 2 3 4 atmod4i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑉 ∈ 𝐴 ∧ ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑉 ≤ 𝑊 ) → ( ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ 𝑉 ) = ( ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∨ 𝑉 ) ∧ 𝑊 ) )
54 18 36 48 51 52 53 syl131anc ⊢ ( 𝜑 → ( ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ 𝑉 ) = ( ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∨ 𝑉 ) ∧ 𝑊 ) )
55 2 4 hlatjass ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∨ 𝑉 ) = ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) )
56 18 20 46 36 55 syl13anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∨ 𝑉 ) = ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) )
57 56 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∨ 𝑉 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) )
58 54 57 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑃 ∨ ( 𝐹 ‘ 𝑃 ) ) ∧ 𝑊 ) ∨ 𝑉 ) = ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) )
59 43 58 eqtrd ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝐹 ) ∨ 𝑉 ) = ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) )
60 39 59 breqtrd ⊢ ( 𝜑 → 𝑈 ≤ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) )
61 21 2 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
62 18 46 36 61 syl3anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
63 21 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∈ ( Base ‘ 𝐾 ) )
64 19 23 62 63 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∈ ( Base ‘ 𝐾 ) )
65 21 3 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
66 19 64 51 65 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) )
67 21 1 3 latmlem2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑈 ≤ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) → ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) ) )
68 19 26 66 30 67 syl13anc ⊢ ( 𝜑 → ( 𝑈 ≤ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) → ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) ) )
69 60 68 mpd ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑈 ) ∧ 𝑈 ) ≤ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) )
70 33 69 eqbrtrrd ⊢ ( 𝜑 → 𝑈 ≤ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) )
71 1 2 3 4 5 6 7 trlval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝑅 ‘ 𝐺 ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) )
72 9 16 12 71 syl3anc ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐺 ) = ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) )
73 17 8 eqtrdi ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑃 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) )
74 73 oveq2d ⊢ ( 𝜑 → ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) = ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) )
75 74 oveq1d ⊢ ( 𝜑 → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) ∧ 𝑊 ) )
76 1 2 4 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑃 ∨ 𝑈 ) )
77 18 20 24 76 syl3anc ⊢ ( 𝜑 → 𝑃 ≤ ( 𝑃 ∨ 𝑈 ) )
78 21 1 2 3 4 atmod3i1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑃 ≤ ( 𝑃 ∨ 𝑈 ) ) → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) )
79 18 20 30 62 77 78 syl131anc ⊢ ( 𝜑 → ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) )
80 79 oveq1d ⊢ ( 𝜑 → ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) ∧ 𝑊 ) = ( ( ( 𝑃 ∨ 𝑈 ) ∧ ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) ∧ 𝑊 ) )
81 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
82 18 81 syl ⊢ ( 𝜑 → 𝐾 ∈ OL )
83 21 3 latmassOLD ⊢ ( ( 𝐾 ∈ OL ∧ ( ( 𝑃 ∨ 𝑈 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ 𝑈 ) ∧ ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) )
84 82 30 64 51 83 syl13anc ⊢ ( 𝜑 → ( ( ( 𝑃 ∨ 𝑈 ) ∧ ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) )
85 80 84 eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ∨ ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) )
86 75 85 eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ∨ ( 𝐺 ‘ 𝑃 ) ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) )
87 72 86 eqtrd ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐺 ) = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) )
88 87 eqcomd ⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝑃 ∨ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) ) ∧ 𝑊 ) ) = ( 𝑅 ‘ 𝐺 ) )
89 70 88 breqtrd ⊢ ( 𝜑 → 𝑈 ≤ ( 𝑅 ‘ 𝐺 ) )
90 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
91 18 90 syl ⊢ ( 𝜑 → 𝐾 ∈ AtLat )
92 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
93 18 92 syl ⊢ ( 𝜑 → 𝐾 ∈ OP )
94 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
95 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
96 94 95 4 0ltat ⊢ ( ( 𝐾 ∈ OP ∧ 𝑈 ∈ 𝐴 ) → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑈 )
97 93 24 96 syl2anc ⊢ ( 𝜑 → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑈 )
98 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
99 18 98 syl ⊢ ( 𝜑 → 𝐾 ∈ Poset )
100 21 94 op0cl ⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
101 93 100 syl ⊢ ( 𝜑 → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
102 21 5 6 7 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
103 9 16 102 syl2anc ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) )
104 21 1 95 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑈 ∧ 𝑈 ≤ ( 𝑅 ‘ 𝐺 ) ) → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑅 ‘ 𝐺 ) ) )
105 99 101 26 103 104 syl13anc ⊢ ( 𝜑 → ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑈 ∧ 𝑈 ≤ ( 𝑅 ‘ 𝐺 ) ) → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑅 ‘ 𝐺 ) ) )
106 97 89 105 mp2and ⊢ ( 𝜑 → ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑅 ‘ 𝐺 ) )
107 21 95 94 opltn0 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑅 ‘ 𝐺 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑅 ‘ 𝐺 ) ↔ ( 𝑅 ‘ 𝐺 ) ≠ ( 0. ‘ 𝐾 ) ) )
108 93 103 107 syl2anc ⊢ ( 𝜑 → ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) ( 𝑅 ‘ 𝐺 ) ↔ ( 𝑅 ‘ 𝐺 ) ≠ ( 0. ‘ 𝐾 ) ) )
109 106 108 mpbid ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐺 ) ≠ ( 0. ‘ 𝐾 ) )
110 109 neneqd ⊢ ( 𝜑 → ¬ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) )
111 94 4 5 6 7 trlator0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐺 ∈ 𝑇 ) → ( ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ∨ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) )
112 9 16 111 syl2anc ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ∨ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ) )
113 112 orcomd ⊢ ( 𝜑 → ( ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) ∨ ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ) )
114 113 ord ⊢ ( 𝜑 → ( ¬ ( 𝑅 ‘ 𝐺 ) = ( 0. ‘ 𝐾 ) → ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ) )
115 110 114 mpd ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 )
116 1 4 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑈 ∈ 𝐴 ∧ ( 𝑅 ‘ 𝐺 ) ∈ 𝐴 ) → ( 𝑈 ≤ ( 𝑅 ‘ 𝐺 ) ↔ 𝑈 = ( 𝑅 ‘ 𝐺 ) ) )
117 91 24 115 116 syl3anc ⊢ ( 𝜑 → ( 𝑈 ≤ ( 𝑅 ‘ 𝐺 ) ↔ 𝑈 = ( 𝑅 ‘ 𝐺 ) ) )
118 89 117 mpbid ⊢ ( 𝜑 → 𝑈 = ( 𝑅 ‘ 𝐺 ) )
119 118 eqcomd ⊢ ( 𝜑 → ( 𝑅 ‘ 𝐺 ) = 𝑈 )