Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdlemg42 Structured version   Visualization version   GIF version
Theorem cdlemg42 40230
Description: Part of proof of Lemma G of [Crawley] p. 116, first line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.)
Hypotheses
Ref Expression
cdlemg42.l ≀ = (leβ€˜πΎ)
cdlemg42.j ∨ = (joinβ€˜πΎ)
cdlemg42.a 𝐴 = (Atomsβ€˜πΎ)
cdlemg42.h 𝐻 = (LHypβ€˜πΎ)
cdlemg42.t 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
cdlemg42.r 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
Assertion
Ref Expression
cdlemg42 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ Β¬ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)))
Proof of Theorem cdlemg42
StepHypRef Expression
1 simp33 1208 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))
2 simpl1l 1221 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ 𝐾 ∈ HL)
3 simp31l 1293 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ 𝑃 ∈ 𝐴)
43adantr 479 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ 𝑃 ∈ 𝐴)
5 simp1 1133 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
6 simp2l 1196 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ 𝐹 ∈ 𝑇)
7 cdlemg42.l . . . . . . . . . . . 12 ≀ = (leβ€˜πΎ)
8 cdlemg42.a . . . . . . . . . . . 12 𝐴 = (Atomsβ€˜πΎ)
9 cdlemg42.h . . . . . . . . . . . 12 𝐻 = (LHypβ€˜πΎ)
10 cdlemg42.t . . . . . . . . . . . 12 𝑇 = ((LTrnβ€˜πΎ)β€˜π‘Š)
117, 8, 9, 10ltrnat 39641 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) β†’ (πΉβ€˜π‘ƒ) ∈ 𝐴)
125, 6, 3, 11syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ (πΉβ€˜π‘ƒ) ∈ 𝐴)
1312adantr 479 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (πΉβ€˜π‘ƒ) ∈ 𝐴)
14 cdlemg42.j . . . . . . . . . 10 ∨ = (joinβ€˜πΎ)
157, 14, 8hlatlej1 38875 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴) β†’ 𝑃 ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)))
162, 4, 13, 15syl3anc 1368 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ 𝑃 ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)))
17 simpr 483 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)))
182hllatd 38864 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ 𝐾 ∈ Lat)
19 eqid 2725 . . . . . . . . . . 11 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
2019, 8atbase 38789 . . . . . . . . . 10 (𝑃 ∈ 𝐴 β†’ 𝑃 ∈ (Baseβ€˜πΎ))
214, 20syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ 𝑃 ∈ (Baseβ€˜πΎ))
22 simp2r 1197 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ 𝐺 ∈ 𝑇)
237, 8, 9, 10ltrnat 39641 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ 𝐴) β†’ (πΊβ€˜π‘ƒ) ∈ 𝐴)
245, 22, 3, 23syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ (πΊβ€˜π‘ƒ) ∈ 𝐴)
2524adantr 479 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (πΊβ€˜π‘ƒ) ∈ 𝐴)
2619, 8atbase 38789 . . . . . . . . . 10 ((πΊβ€˜π‘ƒ) ∈ 𝐴 β†’ (πΊβ€˜π‘ƒ) ∈ (Baseβ€˜πΎ))
2725, 26syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (πΊβ€˜π‘ƒ) ∈ (Baseβ€˜πΎ))
2819, 14, 8hlatjcl 38867 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴) β†’ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
292, 4, 13, 28syl3anc 1368 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))
3019, 7, 14latjle12 18439 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Baseβ€˜πΎ) ∧ (πΊβ€˜π‘ƒ) ∈ (Baseβ€˜πΎ) ∧ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∈ (Baseβ€˜πΎ))) β†’ ((𝑃 ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) ↔ (𝑃 ∨ (πΊβ€˜π‘ƒ)) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))))
3118, 21, 27, 29, 30syl13anc 1369 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ ((𝑃 ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) ↔ (𝑃 ∨ (πΊβ€˜π‘ƒ)) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))))
3216, 17, 31mpbi2and 710 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (𝑃 ∨ (πΊβ€˜π‘ƒ)) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)))
33 simpl32 1252 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (πΊβ€˜π‘ƒ) β‰  𝑃)
3433necomd 2986 . . . . . . . 8 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ 𝑃 β‰  (πΊβ€˜π‘ƒ))
357, 14, 8ps-1 38978 . . . . . . . 8 ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ (πΊβ€˜π‘ƒ) ∈ 𝐴 ∧ 𝑃 β‰  (πΊβ€˜π‘ƒ)) ∧ (𝑃 ∈ 𝐴 ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴)) β†’ ((𝑃 ∨ (πΊβ€˜π‘ƒ)) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ↔ (𝑃 ∨ (πΊβ€˜π‘ƒ)) = (𝑃 ∨ (πΉβ€˜π‘ƒ))))
362, 4, 25, 34, 4, 13, 35syl132anc 1385 . . . . . . 7 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ ((𝑃 ∨ (πΊβ€˜π‘ƒ)) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)) ↔ (𝑃 ∨ (πΊβ€˜π‘ƒ)) = (𝑃 ∨ (πΉβ€˜π‘ƒ))))
3732, 36mpbid 231 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (𝑃 ∨ (πΊβ€˜π‘ƒ)) = (𝑃 ∨ (πΉβ€˜π‘ƒ)))
3837oveq1d 7429 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ ((𝑃 ∨ (πΊβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š) = ((𝑃 ∨ (πΉβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š))
39 simpl1 1188 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (𝐾 ∈ HL ∧ π‘Š ∈ 𝐻))
40 simpl2r 1224 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ 𝐺 ∈ 𝑇)
41 simpl31 1251 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š))
42 eqid 2725 . . . . . . 7 (meetβ€˜πΎ) = (meetβ€˜πΎ)
43 cdlemg42.r . . . . . . 7 𝑅 = ((trLβ€˜πΎ)β€˜π‘Š)
447, 14, 42, 8, 9, 10, 43trlval2 39664 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ (π‘…β€˜πΊ) = ((𝑃 ∨ (πΊβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š))
4539, 40, 41, 44syl3anc 1368 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (π‘…β€˜πΊ) = ((𝑃 ∨ (πΊβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š))
46 simpl2l 1223 . . . . . 6 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ 𝐹 ∈ 𝑇)
477, 14, 42, 8, 9, 10, 43trlval2 39664 . . . . . 6 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š)) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š))
4839, 46, 41, 47syl3anc 1368 . . . . 5 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (π‘…β€˜πΉ) = ((𝑃 ∨ (πΉβ€˜π‘ƒ))(meetβ€˜πΎ)π‘Š))
4938, 45, 483eqtr4rd 2776 . . . 4 ((((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) ∧ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))) β†’ (π‘…β€˜πΉ) = (π‘…β€˜πΊ))
5049ex 411 . . 3 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ ((πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)) β†’ (π‘…β€˜πΉ) = (π‘…β€˜πΊ)))
5150necon3ad 2943 . 2 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ ((π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ) β†’ Β¬ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ))))
521, 51mpd 15 1 (((𝐾 ∈ HL ∧ π‘Š ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ Β¬ 𝑃 ≀ π‘Š) ∧ (πΊβ€˜π‘ƒ) β‰  𝑃 ∧ (π‘…β€˜πΉ) β‰  (π‘…β€˜πΊ))) β†’ Β¬ (πΊβ€˜π‘ƒ) ≀ (𝑃 ∨ (πΉβ€˜π‘ƒ)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098   β‰  wne 2930   class class class wbr 5141  β€˜cfv 6541  (class class class)co 7414  Basecbs 17177  lecple 17237  joincjn 18300  meetcmee 18301  Latclat 18420  Atomscatm 38763  HLchlt 38850  LHypclh 39485  LTrncltrn 39602  trLctrl 39659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5357  ax-pr 5421  ax-un 7736
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-nul 4317  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-map 8843  df-proset 18284  df-poset 18302  df-plt 18319  df-lub 18335  df-glb 18336  df-join 18337  df-meet 18338  df-p0 18414  df-lat 18421  df-oposet 38676  df-ol 38678  df-oml 38679  df-covers 38766  df-ats 38767  df-atl 38798  df-cvlat 38822  df-hlat 38851  df-lhyp 39489  df-laut 39490  df-ldil 39605  df-ltrn 39606  df-trl 39660
This theorem is referenced by:  cdlemg43  40231
  Copyright terms: Public domain W3C validator