This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dia2dimlem3

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

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

Proof

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