Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dia2dimlem3 Structured version   Visualization version   GIF version

Theorem dia2dimlem3 40029
Description: Lemma for dia2dim 40040. Define a translation 𝐷 whose trace is atom 𝑉. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.)
Hypotheses
Ref Expression
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
Ref Expression
dia2dimlem3 (πœ‘ β†’ (π‘…β€˜π·) = 𝑉)

Proof of Theorem dia2dimlem3
StepHypRef Expression
1 dia2dimlem3.k . . . . . . 7 (πœ‘ β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
21simpld 495 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ HL)
3 dia2dimlem3.f . . . . . . . . 9 (πœ‘ β†’ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) β‰  𝑃))
43simpld 495 . . . . . . . 8 (πœ‘ β†’ 𝐹 ∈ 𝑇)
5 dia2dimlem3.p . . . . . . . 8 (πœ‘ β†’ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š))
6 dia2dimlem3.l . . . . . . . . 9 ≀ = (leβ€˜πΎ)
7 dia2dimlem3.a . . . . . . . . 9 𝐴 = (Atomsβ€˜πΎ)
8 dia2dimlem3.h . . . . . . . . 9 𝐻 = (LHypβ€˜πΎ)
9 dia2dimlem3.t . . . . . . . . 9 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
106, 7, 8, 9ltrnel 39102 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ ((πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ Β¬ (πΉβ€˜π‘ƒ) ≀ π‘Š))
111, 4, 5, 10syl3anc 1371 . . . . . . 7 (πœ‘ β†’ ((πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ Β¬ (πΉβ€˜π‘ƒ) ≀ π‘Š))
1211simpld 495 . . . . . 6 (πœ‘ β†’ (πΉβ€˜π‘ƒ) ∈ 𝐴)
13 dia2dimlem3.v . . . . . . 7 (πœ‘ β†’ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š))
1413simpld 495 . . . . . 6 (πœ‘ β†’ 𝑉 ∈ 𝐴)
15 dia2dimlem3.j . . . . . . 7 ∨ = (joinβ€˜πΎ)
166, 15, 7hlatlej2 38338 . . . . . 6 ((𝐾 ∈ HL ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ 𝑉 ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉))
172, 12, 14, 16syl3anc 1371 . . . . 5 (πœ‘ β†’ 𝑉 ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉))
182hllatd 38326 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ Lat)
19 eqid 2732 . . . . . . . 8 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
2019, 7atbase 38251 . . . . . . 7 (𝑉 ∈ 𝐴 β†’ 𝑉 ∈ (Baseβ€˜πΎ))
2114, 20syl 17 . . . . . 6 (πœ‘ β†’ 𝑉 ∈ (Baseβ€˜πΎ))
2219, 15, 7hlatjcl 38329 . . . . . . 7 ((𝐾 ∈ HL ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ))
232, 12, 14, 22syl3anc 1371 . . . . . 6 (πœ‘ β†’ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ))
24 dia2dimlem3.r . . . . . . . . 9 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
256, 7, 8, 9, 24trlat 39132 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) β‰  𝑃)) β†’ (π‘…β€˜πΉ) ∈ 𝐴)
261, 5, 3, 25syl3anc 1371 . . . . . . 7 (πœ‘ β†’ (π‘…β€˜πΉ) ∈ 𝐴)
27 dia2dimlem3.u . . . . . . . 8 (πœ‘ β†’ (π‘ˆ ∈ 𝐴 ∧ π‘ˆ ≀ π‘Š))
2827simpld 495 . . . . . . 7 (πœ‘ β†’ π‘ˆ ∈ 𝐴)
2919, 15, 7hlatjcl 38329 . . . . . . 7 ((𝐾 ∈ HL ∧ (π‘…β€˜πΉ) ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ ((π‘…β€˜πΉ) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
302, 26, 28, 29syl3anc 1371 . . . . . 6 (πœ‘ β†’ ((π‘…β€˜πΉ) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
31 dia2dimlem3.m . . . . . . 7 ∧ = (meetβ€˜πΎ)
3219, 6, 31latmlem2 18425 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Baseβ€˜πΎ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ) ∧ ((π‘…β€˜πΉ) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))) β†’ (𝑉 ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉) β†’ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) ≀ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉))))
3318, 21, 23, 30, 32syl13anc 1372 . . . . 5 (πœ‘ β†’ (𝑉 ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉) β†’ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) ≀ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉))))
3417, 33mpd 15 . . . 4 (πœ‘ β†’ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) ≀ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
35 dia2dimlem3.rf . . . . . . 7 (πœ‘ β†’ (π‘…β€˜πΉ) ≀ (π‘ˆ ∨ 𝑉))
3615, 7hlatjcom 38330 . . . . . . . 8 ((𝐾 ∈ HL ∧ π‘ˆ ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ (π‘ˆ ∨ 𝑉) = (𝑉 ∨ π‘ˆ))
372, 28, 14, 36syl3anc 1371 . . . . . . 7 (πœ‘ β†’ (π‘ˆ ∨ 𝑉) = (𝑉 ∨ π‘ˆ))
3835, 37breqtrd 5174 . . . . . 6 (πœ‘ β†’ (π‘…β€˜πΉ) ≀ (𝑉 ∨ π‘ˆ))
39 dia2dimlem3.ru . . . . . . 7 (πœ‘ β†’ (π‘…β€˜πΉ) β‰  π‘ˆ)
406, 15, 7hlatexch2 38359 . . . . . . 7 ((𝐾 ∈ HL ∧ ((π‘…β€˜πΉ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (π‘…β€˜πΉ) β‰  π‘ˆ) β†’ ((π‘…β€˜πΉ) ≀ (𝑉 ∨ π‘ˆ) β†’ 𝑉 ≀ ((π‘…β€˜πΉ) ∨ π‘ˆ)))
412, 26, 14, 28, 39, 40syl131anc 1383 . . . . . 6 (πœ‘ β†’ ((π‘…β€˜πΉ) ≀ (𝑉 ∨ π‘ˆ) β†’ 𝑉 ≀ ((π‘…β€˜πΉ) ∨ π‘ˆ)))
4238, 41mpd 15 . . . . 5 (πœ‘ β†’ 𝑉 ≀ ((π‘…β€˜πΉ) ∨ π‘ˆ))
4319, 6, 31latleeqm2 18423 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑉 ∈ (Baseβ€˜πΎ) ∧ ((π‘…β€˜πΉ) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ)) β†’ (𝑉 ≀ ((π‘…β€˜πΉ) ∨ π‘ˆ) ↔ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) = 𝑉))
4418, 21, 30, 43syl3anc 1371 . . . . 5 (πœ‘ β†’ (𝑉 ≀ ((π‘…β€˜πΉ) ∨ π‘ˆ) ↔ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) = 𝑉))
4542, 44mpbid 231 . . . 4 (πœ‘ β†’ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) = 𝑉)
46 dia2dimlem3.d . . . . . 6 (πœ‘ β†’ 𝐷 ∈ 𝑇)
47 dia2dimlem3.q . . . . . . 7 𝑄 = ((𝑃 ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉))
48 dia2dimlem3.uv . . . . . . 7 (πœ‘ β†’ π‘ˆ β‰  𝑉)
496, 15, 31, 7, 8, 9, 24, 47, 1, 27, 13, 5, 3, 35, 48, 39dia2dimlem1 40027 . . . . . 6 (πœ‘ β†’ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š))
506, 15, 31, 7, 8, 9, 24trlval2 39126 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐷 ∈ 𝑇 ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) β†’ (π‘…β€˜π·) = ((𝑄 ∨ (π·β€˜π‘„)) ∧ π‘Š))
511, 46, 49, 50syl3anc 1371 . . . . 5 (πœ‘ β†’ (π‘…β€˜π·) = ((𝑄 ∨ (π·β€˜π‘„)) ∧ π‘Š))
5247a1i 11 . . . . . . . . 9 (πœ‘ β†’ 𝑄 = ((𝑃 ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
53 dia2dimlem3.dv . . . . . . . . 9 (πœ‘ β†’ (π·β€˜π‘„) = (πΉβ€˜π‘ƒ))
5452, 53oveq12d 7429 . . . . . . . 8 (πœ‘ β†’ (𝑄 ∨ (π·β€˜π‘„)) = (((𝑃 ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∨ (πΉβ€˜π‘ƒ)))
555simpld 495 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ 𝐴)
5619, 15, 7hlatjcl 38329 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑃 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
572, 55, 28, 56syl3anc 1371 . . . . . . . . 9 (πœ‘ β†’ (𝑃 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
586, 15, 7hlatlej1 38337 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ (πΉβ€˜π‘ƒ) ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉))
592, 12, 14, 58syl3anc 1371 . . . . . . . . 9 (πœ‘ β†’ (πΉβ€˜π‘ƒ) ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉))
6019, 6, 15, 31, 7atmod4i1 38829 . . . . . . . . 9 ((𝐾 ∈ HL ∧ ((πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ (𝑃 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ)) ∧ (πΉβ€˜π‘ƒ) ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) β†’ (((𝑃 ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∨ (πΉβ€˜π‘ƒ)) = (((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
612, 12, 57, 23, 59, 60syl131anc 1383 . . . . . . . 8 (πœ‘ β†’ (((𝑃 ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∨ (πΉβ€˜π‘ƒ)) = (((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
6215, 7hlatj32 38334 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴 ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴)) β†’ ((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) = ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ))
632, 55, 28, 12, 62syl13anc 1372 . . . . . . . . 9 (πœ‘ β†’ ((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) = ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ))
6463oveq1d 7426 . . . . . . . 8 (πœ‘ β†’ (((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
6554, 61, 643eqtrd 2776 . . . . . . 7 (πœ‘ β†’ (𝑄 ∨ (π·β€˜π‘„)) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
6665oveq1d 7426 . . . . . 6 (πœ‘ β†’ ((𝑄 ∨ (π·β€˜π‘„)) ∧ π‘Š) = ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∧ π‘Š))
67 hlol 38323 . . . . . . . 8 (𝐾 ∈ HL β†’ 𝐾 ∈ OL)
682, 67syl 17 . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ OL)
6919, 15, 7hlatjcl 38329 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴) β†’ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
702, 55, 12, 69syl3anc 1371 . . . . . . . 8 (πœ‘ β†’ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
7119, 7atbase 38251 . . . . . . . . 9 (π‘ˆ ∈ 𝐴 β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
7228, 71syl 17 . . . . . . . 8 (πœ‘ β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
7319, 15latjcl 18394 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
7418, 70, 72, 73syl3anc 1371 . . . . . . 7 (πœ‘ β†’ ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
751simprd 496 . . . . . . . 8 (πœ‘ β†’ π‘Š ∈ 𝐻)
7619, 8lhpbase 38961 . . . . . . . 8 (π‘Š ∈ 𝐻 β†’ π‘Š ∈ (Baseβ€˜πΎ))
7775, 76syl 17 . . . . . . 7 (πœ‘ β†’ π‘Š ∈ (Baseβ€˜πΎ))
7819, 31latm32 38193 . . . . . . 7 ((𝐾 ∈ OL ∧ (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∧ π‘Š) = ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
7968, 74, 23, 77, 78syl13anc 1372 . . . . . 6 (πœ‘ β†’ ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∧ π‘Š) = ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
806, 15, 31, 7, 8, 9, 24trlval2 39126 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š))
811, 4, 5, 80syl3anc 1371 . . . . . . . . 9 (πœ‘ β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š))
8281oveq1d 7426 . . . . . . . 8 (πœ‘ β†’ ((π‘…β€˜πΉ) ∨ π‘ˆ) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š) ∨ π‘ˆ))
8327simprd 496 . . . . . . . . 9 (πœ‘ β†’ π‘ˆ ≀ π‘Š)
8419, 6, 15, 31, 7atmod4i1 38829 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (π‘ˆ ∈ 𝐴 ∧ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) ∧ π‘ˆ ≀ π‘Š) β†’ (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š) ∨ π‘ˆ) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š))
852, 28, 70, 77, 83, 84syl131anc 1383 . . . . . . . 8 (πœ‘ β†’ (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š) ∨ π‘ˆ) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š))
8682, 85eqtr2d 2773 . . . . . . 7 (πœ‘ β†’ (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š) = ((π‘…β€˜πΉ) ∨ π‘ˆ))
8786oveq1d 7426 . . . . . 6 (πœ‘ β†’ ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) = (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
8866, 79, 873eqtrd 2776 . . . . 5 (πœ‘ β†’ ((𝑄 ∨ (π·β€˜π‘„)) ∧ π‘Š) = (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
8951, 88eqtr2d 2773 . . . 4 (πœ‘ β†’ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) = (π‘…β€˜π·))
9034, 45, 893brtr3d 5179 . . 3 (πœ‘ β†’ 𝑉 ≀ (π‘…β€˜π·))
91 hlatl 38322 . . . . 5 (𝐾 ∈ HL β†’ 𝐾 ∈ AtLat)
922, 91syl 17 . . . 4 (πœ‘ β†’ 𝐾 ∈ AtLat)
93 hlop 38324 . . . . . . . . . 10 (𝐾 ∈ HL β†’ 𝐾 ∈ OP)
942, 93syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ OP)
95 eqid 2732 . . . . . . . . . 10 (0.β€˜πΎ) = (0.β€˜πΎ)
96 eqid 2732 . . . . . . . . . 10 (ltβ€˜πΎ) = (ltβ€˜πΎ)
9795, 96, 70ltat 38253 . . . . . . . . 9 ((𝐾 ∈ OP ∧ 𝑉 ∈ 𝐴) β†’ (0.β€˜πΎ)(ltβ€˜πΎ)𝑉)
9894, 14, 97syl2anc 584 . . . . . . . 8 (πœ‘ β†’ (0.β€˜πΎ)(ltβ€˜πΎ)𝑉)
99 hlpos 38328 . . . . . . . . . 10 (𝐾 ∈ HL β†’ 𝐾 ∈ Poset)
1002, 99syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ Poset)
10119, 95op0cl 38146 . . . . . . . . . 10 (𝐾 ∈ OP β†’ (0.β€˜πΎ) ∈ (Baseβ€˜πΎ))
10294, 101syl 17 . . . . . . . . 9 (πœ‘ β†’ (0.β€˜πΎ) ∈ (Baseβ€˜πΎ))
10319, 8, 9, 24trlcl 39127 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐷 ∈ 𝑇) β†’ (π‘…β€˜π·) ∈ (Baseβ€˜πΎ))
1041, 46, 103syl2anc 584 . . . . . . . . 9 (πœ‘ β†’ (π‘…β€˜π·) ∈ (Baseβ€˜πΎ))
10519, 6, 96pltletr 18298 . . . . . . . . 9 ((𝐾 ∈ Poset ∧ ((0.β€˜πΎ) ∈ (Baseβ€˜πΎ) ∧ 𝑉 ∈ (Baseβ€˜πΎ) ∧ (π‘…β€˜π·) ∈ (Baseβ€˜πΎ))) β†’ (((0.β€˜πΎ)(ltβ€˜πΎ)𝑉 ∧ 𝑉 ≀ (π‘…β€˜π·)) β†’ (0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·)))
106100, 102, 21, 104, 105syl13anc 1372 . . . . . . . 8 (πœ‘ β†’ (((0.β€˜πΎ)(ltβ€˜πΎ)𝑉 ∧ 𝑉 ≀ (π‘…β€˜π·)) β†’ (0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·)))
10798, 90, 106mp2and 697 . . . . . . 7 (πœ‘ β†’ (0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·))
10819, 96, 95opltn0 38152 . . . . . . . 8 ((𝐾 ∈ OP ∧ (π‘…β€˜π·) ∈ (Baseβ€˜πΎ)) β†’ ((0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·) ↔ (π‘…β€˜π·) β‰  (0.β€˜πΎ)))
10994, 104, 108syl2anc 584 . . . . . . 7 (πœ‘ β†’ ((0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·) ↔ (π‘…β€˜π·) β‰  (0.β€˜πΎ)))
110107, 109mpbid 231 . . . . . 6 (πœ‘ β†’ (π‘…β€˜π·) β‰  (0.β€˜πΎ))
111110neneqd 2945 . . . . 5 (πœ‘ β†’ Β¬ (π‘…β€˜π·) = (0.β€˜πΎ))
11295, 7, 8, 9, 24trlator0 39134 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐷 ∈ 𝑇) β†’ ((π‘…β€˜π·) ∈ 𝐴 ∨ (π‘…β€˜π·) = (0.β€˜πΎ)))
1131, 46, 112syl2anc 584 . . . . . . 7 (πœ‘ β†’ ((π‘…β€˜π·) ∈ 𝐴 ∨ (π‘…β€˜π·) = (0.β€˜πΎ)))
114113orcomd 869 . . . . . 6 (πœ‘ β†’ ((π‘…β€˜π·) = (0.β€˜πΎ) ∨ (π‘…β€˜π·) ∈ 𝐴))
115114ord 862 . . . . 5 (πœ‘ β†’ (Β¬ (π‘…β€˜π·) = (0.β€˜πΎ) β†’ (π‘…β€˜π·) ∈ 𝐴))
116111, 115mpd 15 . . . 4 (πœ‘ β†’ (π‘…β€˜π·) ∈ 𝐴)
1176, 7atcmp 38273 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑉 ∈ 𝐴 ∧ (π‘…β€˜π·) ∈ 𝐴) β†’ (𝑉 ≀ (π‘…β€˜π·) ↔ 𝑉 = (π‘…β€˜π·)))
11892, 14, 116, 117syl3anc 1371 . . 3 (πœ‘ β†’ (𝑉 ≀ (π‘…β€˜π·) ↔ 𝑉 = (π‘…β€˜π·)))
11990, 118mpbid 231 . 2 (πœ‘ β†’ 𝑉 = (π‘…β€˜π·))
120119eqcomd 2738 1 (πœ‘ β†’ (π‘…β€˜π·) = 𝑉)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   β‰  wne 2940   class class class wbr 5148  β€˜cfv 6543  (class class class)co 7411  Basecbs 17146  lecple 17206  Posetcpo 18262  ltcplt 18263  joincjn 18266  meetcmee 18267  0.cp0 18378  Latclat 18386  OPcops 38134  OLcol 38136  Atomscatm 38225  AtLatcal 38226  HLchlt 38312  LHypclh 38947  LTrncltrn 39064  trLctrl 39121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-map 8824  df-proset 18250  df-poset 18268  df-plt 18285  df-lub 18301  df-glb 18302  df-join 18303  df-meet 18304  df-p0 18380  df-p1 18381  df-lat 18387  df-clat 18454  df-oposet 38138  df-ol 38140  df-oml 38141  df-covers 38228  df-ats 38229  df-atl 38260  df-cvlat 38284  df-hlat 38313  df-llines 38461  df-psubsp 38466  df-pmap 38467  df-padd 38759  df-lhyp 38951  df-laut 38952  df-ldil 39067  df-ltrn 39068  df-trl 39122
This theorem is referenced by:  dia2dimlem5  40031
  Copyright terms: Public domain W3C validator