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 39532
Description: Lemma for dia2dim 39543. 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 496 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ HL)
3 dia2dimlem3.f . . . . . . . . 9 (πœ‘ β†’ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) β‰  𝑃))
43simpld 496 . . . . . . . 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 38605 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ ((πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ Β¬ (πΉβ€˜π‘ƒ) ≀ π‘Š))
111, 4, 5, 10syl3anc 1372 . . . . . . 7 (πœ‘ β†’ ((πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ Β¬ (πΉβ€˜π‘ƒ) ≀ π‘Š))
1211simpld 496 . . . . . 6 (πœ‘ β†’ (πΉβ€˜π‘ƒ) ∈ 𝐴)
13 dia2dimlem3.v . . . . . . 7 (πœ‘ β†’ (𝑉 ∈ 𝐴 ∧ 𝑉 ≀ π‘Š))
1413simpld 496 . . . . . 6 (πœ‘ β†’ 𝑉 ∈ 𝐴)
15 dia2dimlem3.j . . . . . . 7 ∨ = (joinβ€˜πΎ)
166, 15, 7hlatlej2 37841 . . . . . 6 ((𝐾 ∈ HL ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ 𝑉 ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉))
172, 12, 14, 16syl3anc 1372 . . . . 5 (πœ‘ β†’ 𝑉 ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉))
182hllatd 37829 . . . . . 6 (πœ‘ β†’ 𝐾 ∈ Lat)
19 eqid 2737 . . . . . . . 8 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
2019, 7atbase 37754 . . . . . . 7 (𝑉 ∈ 𝐴 β†’ 𝑉 ∈ (Baseβ€˜πΎ))
2114, 20syl 17 . . . . . 6 (πœ‘ β†’ 𝑉 ∈ (Baseβ€˜πΎ))
2219, 15, 7hlatjcl 37832 . . . . . . 7 ((𝐾 ∈ HL ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ))
232, 12, 14, 22syl3anc 1372 . . . . . 6 (πœ‘ β†’ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ))
24 dia2dimlem3.r . . . . . . . . 9 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
256, 7, 8, 9, 24trlat 38635 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (𝐹 ∈ 𝑇 ∧ (πΉβ€˜π‘ƒ) β‰  𝑃)) β†’ (π‘…β€˜πΉ) ∈ 𝐴)
261, 5, 3, 25syl3anc 1372 . . . . . . 7 (πœ‘ β†’ (π‘…β€˜πΉ) ∈ 𝐴)
27 dia2dimlem3.u . . . . . . . 8 (πœ‘ β†’ (π‘ˆ ∈ 𝐴 ∧ π‘ˆ ≀ π‘Š))
2827simpld 496 . . . . . . 7 (πœ‘ β†’ π‘ˆ ∈ 𝐴)
2919, 15, 7hlatjcl 37832 . . . . . . 7 ((𝐾 ∈ HL ∧ (π‘…β€˜πΉ) ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ ((π‘…β€˜πΉ) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
302, 26, 28, 29syl3anc 1372 . . . . . 6 (πœ‘ β†’ ((π‘…β€˜πΉ) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
31 dia2dimlem3.m . . . . . . 7 ∧ = (meetβ€˜πΎ)
3219, 6, 31latmlem2 18360 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Baseβ€˜πΎ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ) ∧ ((π‘…β€˜πΉ) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))) β†’ (𝑉 ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉) β†’ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) ≀ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉))))
3318, 21, 23, 30, 32syl13anc 1373 . . . . 5 (πœ‘ β†’ (𝑉 ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉) β†’ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) ≀ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉))))
3417, 33mpd 15 . . . 4 (πœ‘ β†’ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) ≀ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
35 dia2dimlem3.rf . . . . . . 7 (πœ‘ β†’ (π‘…β€˜πΉ) ≀ (π‘ˆ ∨ 𝑉))
3615, 7hlatjcom 37833 . . . . . . . 8 ((𝐾 ∈ HL ∧ π‘ˆ ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ (π‘ˆ ∨ 𝑉) = (𝑉 ∨ π‘ˆ))
372, 28, 14, 36syl3anc 1372 . . . . . . 7 (πœ‘ β†’ (π‘ˆ ∨ 𝑉) = (𝑉 ∨ π‘ˆ))
3835, 37breqtrd 5132 . . . . . 6 (πœ‘ β†’ (π‘…β€˜πΉ) ≀ (𝑉 ∨ π‘ˆ))
39 dia2dimlem3.ru . . . . . . 7 (πœ‘ β†’ (π‘…β€˜πΉ) β‰  π‘ˆ)
406, 15, 7hlatexch2 37862 . . . . . . 7 ((𝐾 ∈ HL ∧ ((π‘…β€˜πΉ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) ∧ (π‘…β€˜πΉ) β‰  π‘ˆ) β†’ ((π‘…β€˜πΉ) ≀ (𝑉 ∨ π‘ˆ) β†’ 𝑉 ≀ ((π‘…β€˜πΉ) ∨ π‘ˆ)))
412, 26, 14, 28, 39, 40syl131anc 1384 . . . . . 6 (πœ‘ β†’ ((π‘…β€˜πΉ) ≀ (𝑉 ∨ π‘ˆ) β†’ 𝑉 ≀ ((π‘…β€˜πΉ) ∨ π‘ˆ)))
4238, 41mpd 15 . . . . 5 (πœ‘ β†’ 𝑉 ≀ ((π‘…β€˜πΉ) ∨ π‘ˆ))
4319, 6, 31latleeqm2 18358 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑉 ∈ (Baseβ€˜πΎ) ∧ ((π‘…β€˜πΉ) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ)) β†’ (𝑉 ≀ ((π‘…β€˜πΉ) ∨ π‘ˆ) ↔ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ 𝑉) = 𝑉))
4418, 21, 30, 43syl3anc 1372 . . . . 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 39530 . . . . . 6 (πœ‘ β†’ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š))
506, 15, 31, 7, 8, 9, 24trlval2 38629 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐷 ∈ 𝑇 ∧ (𝑄 ∈ 𝐴 ∧ Β¬ 𝑄 ≀ π‘Š)) β†’ (π‘…β€˜π·) = ((𝑄 ∨ (π·β€˜π‘„)) ∧ π‘Š))
511, 46, 49, 50syl3anc 1372 . . . . 5 (πœ‘ β†’ (π‘…β€˜π·) = ((𝑄 ∨ (π·β€˜π‘„)) ∧ π‘Š))
5247a1i 11 . . . . . . . . 9 (πœ‘ β†’ 𝑄 = ((𝑃 ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
53 dia2dimlem3.dv . . . . . . . . 9 (πœ‘ β†’ (π·β€˜π‘„) = (πΉβ€˜π‘ƒ))
5452, 53oveq12d 7376 . . . . . . . 8 (πœ‘ β†’ (𝑄 ∨ (π·β€˜π‘„)) = (((𝑃 ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∨ (πΉβ€˜π‘ƒ)))
555simpld 496 . . . . . . . . . 10 (πœ‘ β†’ 𝑃 ∈ 𝐴)
5619, 15, 7hlatjcl 37832 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴) β†’ (𝑃 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
572, 55, 28, 56syl3anc 1372 . . . . . . . . 9 (πœ‘ β†’ (𝑃 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
586, 15, 7hlatlej1 37840 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) β†’ (πΉβ€˜π‘ƒ) ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉))
592, 12, 14, 58syl3anc 1372 . . . . . . . . 9 (πœ‘ β†’ (πΉβ€˜π‘ƒ) ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉))
6019, 6, 15, 31, 7atmod4i1 38332 . . . . . . . . 9 ((𝐾 ∈ HL ∧ ((πΉβ€˜π‘ƒ) ∈ 𝐴 ∧ (𝑃 ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ)) ∧ (πΉβ€˜π‘ƒ) ≀ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) β†’ (((𝑃 ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∨ (πΉβ€˜π‘ƒ)) = (((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
612, 12, 57, 23, 59, 60syl131anc 1384 . . . . . . . 8 (πœ‘ β†’ (((𝑃 ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∨ (πΉβ€˜π‘ƒ)) = (((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
6215, 7hlatj32 37837 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ π‘ˆ ∈ 𝐴 ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴)) β†’ ((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) = ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ))
632, 55, 28, 12, 62syl13anc 1373 . . . . . . . . 9 (πœ‘ β†’ ((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) = ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ))
6463oveq1d 7373 . . . . . . . 8 (πœ‘ β†’ (((𝑃 ∨ π‘ˆ) ∨ (πΉβ€˜π‘ƒ)) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
6554, 61, 643eqtrd 2781 . . . . . . 7 (πœ‘ β†’ (𝑄 ∨ (π·β€˜π‘„)) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
6665oveq1d 7373 . . . . . 6 (πœ‘ β†’ ((𝑄 ∨ (π·β€˜π‘„)) ∧ π‘Š) = ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∧ π‘Š))
67 hlol 37826 . . . . . . . 8 (𝐾 ∈ HL β†’ 𝐾 ∈ OL)
682, 67syl 17 . . . . . . 7 (πœ‘ β†’ 𝐾 ∈ OL)
6919, 15, 7hlatjcl 37832 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴) β†’ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
702, 55, 12, 69syl3anc 1372 . . . . . . . 8 (πœ‘ β†’ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
7119, 7atbase 37754 . . . . . . . . 9 (π‘ˆ ∈ 𝐴 β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
7228, 71syl 17 . . . . . . . 8 (πœ‘ β†’ π‘ˆ ∈ (Baseβ€˜πΎ))
7319, 15latjcl 18329 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ) ∧ π‘ˆ ∈ (Baseβ€˜πΎ)) β†’ ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
7418, 70, 72, 73syl3anc 1372 . . . . . . 7 (πœ‘ β†’ ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ))
751simprd 497 . . . . . . . 8 (πœ‘ β†’ π‘Š ∈ 𝐻)
7619, 8lhpbase 38464 . . . . . . . 8 (π‘Š ∈ 𝐻 β†’ π‘Š ∈ (Baseβ€˜πΎ))
7775, 76syl 17 . . . . . . 7 (πœ‘ β†’ π‘Š ∈ (Baseβ€˜πΎ))
7819, 31latm32 37696 . . . . . . 7 ((𝐾 ∈ OL ∧ (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∈ (Baseβ€˜πΎ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ))) β†’ ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∧ π‘Š) = ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
7968, 74, 23, 77, 78syl13anc 1373 . . . . . 6 (πœ‘ β†’ ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) ∧ π‘Š) = ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
806, 15, 31, 7, 8, 9, 24trlval2 38629 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š))
811, 4, 5, 80syl3anc 1372 . . . . . . . . 9 (πœ‘ β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š))
8281oveq1d 7373 . . . . . . . 8 (πœ‘ β†’ ((π‘…β€˜πΉ) ∨ π‘ˆ) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š) ∨ π‘ˆ))
8327simprd 497 . . . . . . . . 9 (πœ‘ β†’ π‘ˆ ≀ π‘Š)
8419, 6, 15, 31, 7atmod4i1 38332 . . . . . . . . 9 ((𝐾 ∈ HL ∧ (π‘ˆ ∈ 𝐴 ∧ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ) ∧ π‘Š ∈ (Baseβ€˜πΎ)) ∧ π‘ˆ ≀ π‘Š) β†’ (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š) ∨ π‘ˆ) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š))
852, 28, 70, 77, 83, 84syl131anc 1384 . . . . . . . 8 (πœ‘ β†’ (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ π‘Š) ∨ π‘ˆ) = (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š))
8682, 85eqtr2d 2778 . . . . . . 7 (πœ‘ β†’ (((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š) = ((π‘…β€˜πΉ) ∨ π‘ˆ))
8786oveq1d 7373 . . . . . 6 (πœ‘ β†’ ((((𝑃 ∨ (πΉβ€˜π‘ƒ)) ∨ π‘ˆ) ∧ π‘Š) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) = (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
8866, 79, 873eqtrd 2781 . . . . 5 (πœ‘ β†’ ((𝑄 ∨ (π·β€˜π‘„)) ∧ π‘Š) = (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)))
8951, 88eqtr2d 2778 . . . 4 (πœ‘ β†’ (((π‘…β€˜πΉ) ∨ π‘ˆ) ∧ ((πΉβ€˜π‘ƒ) ∨ 𝑉)) = (π‘…β€˜π·))
9034, 45, 893brtr3d 5137 . . 3 (πœ‘ β†’ 𝑉 ≀ (π‘…β€˜π·))
91 hlatl 37825 . . . . 5 (𝐾 ∈ HL β†’ 𝐾 ∈ AtLat)
922, 91syl 17 . . . 4 (πœ‘ β†’ 𝐾 ∈ AtLat)
93 hlop 37827 . . . . . . . . . 10 (𝐾 ∈ HL β†’ 𝐾 ∈ OP)
942, 93syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ OP)
95 eqid 2737 . . . . . . . . . 10 (0.β€˜πΎ) = (0.β€˜πΎ)
96 eqid 2737 . . . . . . . . . 10 (ltβ€˜πΎ) = (ltβ€˜πΎ)
9795, 96, 70ltat 37756 . . . . . . . . 9 ((𝐾 ∈ OP ∧ 𝑉 ∈ 𝐴) β†’ (0.β€˜πΎ)(ltβ€˜πΎ)𝑉)
9894, 14, 97syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (0.β€˜πΎ)(ltβ€˜πΎ)𝑉)
99 hlpos 37831 . . . . . . . . . 10 (𝐾 ∈ HL β†’ 𝐾 ∈ Poset)
1002, 99syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝐾 ∈ Poset)
10119, 95op0cl 37649 . . . . . . . . . 10 (𝐾 ∈ OP β†’ (0.β€˜πΎ) ∈ (Baseβ€˜πΎ))
10294, 101syl 17 . . . . . . . . 9 (πœ‘ β†’ (0.β€˜πΎ) ∈ (Baseβ€˜πΎ))
10319, 8, 9, 24trlcl 38630 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐷 ∈ 𝑇) β†’ (π‘…β€˜π·) ∈ (Baseβ€˜πΎ))
1041, 46, 103syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (π‘…β€˜π·) ∈ (Baseβ€˜πΎ))
10519, 6, 96pltletr 18233 . . . . . . . . 9 ((𝐾 ∈ Poset ∧ ((0.β€˜πΎ) ∈ (Baseβ€˜πΎ) ∧ 𝑉 ∈ (Baseβ€˜πΎ) ∧ (π‘…β€˜π·) ∈ (Baseβ€˜πΎ))) β†’ (((0.β€˜πΎ)(ltβ€˜πΎ)𝑉 ∧ 𝑉 ≀ (π‘…β€˜π·)) β†’ (0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·)))
106100, 102, 21, 104, 105syl13anc 1373 . . . . . . . 8 (πœ‘ β†’ (((0.β€˜πΎ)(ltβ€˜πΎ)𝑉 ∧ 𝑉 ≀ (π‘…β€˜π·)) β†’ (0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·)))
10798, 90, 106mp2and 698 . . . . . . 7 (πœ‘ β†’ (0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·))
10819, 96, 95opltn0 37655 . . . . . . . 8 ((𝐾 ∈ OP ∧ (π‘…β€˜π·) ∈ (Baseβ€˜πΎ)) β†’ ((0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·) ↔ (π‘…β€˜π·) β‰  (0.β€˜πΎ)))
10994, 104, 108syl2anc 585 . . . . . . 7 (πœ‘ β†’ ((0.β€˜πΎ)(ltβ€˜πΎ)(π‘…β€˜π·) ↔ (π‘…β€˜π·) β‰  (0.β€˜πΎ)))
110107, 109mpbid 231 . . . . . 6 (πœ‘ β†’ (π‘…β€˜π·) β‰  (0.β€˜πΎ))
111110neneqd 2949 . . . . 5 (πœ‘ β†’ Β¬ (π‘…β€˜π·) = (0.β€˜πΎ))
11295, 7, 8, 9, 24trlator0 38637 . . . . . . . 8 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐷 ∈ 𝑇) β†’ ((π‘…β€˜π·) ∈ 𝐴 ∨ (π‘…β€˜π·) = (0.β€˜πΎ)))
1131, 46, 112syl2anc 585 . . . . . . 7 (πœ‘ β†’ ((π‘…β€˜π·) ∈ 𝐴 ∨ (π‘…β€˜π·) = (0.β€˜πΎ)))
114113orcomd 870 . . . . . 6 (πœ‘ β†’ ((π‘…β€˜π·) = (0.β€˜πΎ) ∨ (π‘…β€˜π·) ∈ 𝐴))
115114ord 863 . . . . 5 (πœ‘ β†’ (Β¬ (π‘…β€˜π·) = (0.β€˜πΎ) β†’ (π‘…β€˜π·) ∈ 𝐴))
116111, 115mpd 15 . . . 4 (πœ‘ β†’ (π‘…β€˜π·) ∈ 𝐴)
1176, 7atcmp 37776 . . . 4 ((𝐾 ∈ AtLat ∧ 𝑉 ∈ 𝐴 ∧ (π‘…β€˜π·) ∈ 𝐴) β†’ (𝑉 ≀ (π‘…β€˜π·) ↔ 𝑉 = (π‘…β€˜π·)))
11892, 14, 116, 117syl3anc 1372 . . 3 (πœ‘ β†’ (𝑉 ≀ (π‘…β€˜π·) ↔ 𝑉 = (π‘…β€˜π·)))
11990, 118mpbid 231 . 2 (πœ‘ β†’ 𝑉 = (π‘…β€˜π·))
120119eqcomd 2743 1 (πœ‘ β†’ (π‘…β€˜π·) = 𝑉)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   β‰  wne 2944   class class class wbr 5106  β€˜cfv 6497  (class class class)co 7358  Basecbs 17084  lecple 17141  Posetcpo 18197  ltcplt 18198  joincjn 18201  meetcmee 18202  0.cp0 18313  Latclat 18321  OPcops 37637  OLcol 37639  Atomscatm 37728  AtLatcal 37729  HLchlt 37815  LHypclh 38450  LTrncltrn 38567  trLctrl 38624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-map 8768  df-proset 18185  df-poset 18203  df-plt 18220  df-lub 18236  df-glb 18237  df-join 18238  df-meet 18239  df-p0 18315  df-p1 18316  df-lat 18322  df-clat 18389  df-oposet 37641  df-ol 37643  df-oml 37644  df-covers 37731  df-ats 37732  df-atl 37763  df-cvlat 37787  df-hlat 37816  df-llines 37964  df-psubsp 37969  df-pmap 37970  df-padd 38262  df-lhyp 38454  df-laut 38455  df-ldil 38570  df-ltrn 38571  df-trl 38625
This theorem is referenced by:  dia2dimlem5  39534
  Copyright terms: Public domain W3C validator