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

Theorem cdlemi 38381
 Description: Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)
Hypotheses
Ref Expression
cdlemi.b 𝐵 = (Base‘𝐾)
cdlemi.l = (le‘𝐾)
cdlemi.j = (join‘𝐾)
cdlemi.m = (meet‘𝐾)
cdlemi.a 𝐴 = (Atoms‘𝐾)
cdlemi.h 𝐻 = (LHyp‘𝐾)
cdlemi.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemi.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemi.e 𝐸 = ((TEndo‘𝐾)‘𝑊)
cdlemi.s 𝑆 = ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))))
Assertion
Ref Expression
cdlemi ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐺)‘𝑃) = 𝑆)

Proof of Theorem cdlemi
StepHypRef Expression
1 simp11l 1282 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝐾 ∈ HL)
2 simp11r 1283 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝑊𝐻)
3 simp2l 1197 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝑈𝐸)
4 simp13 1203 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝐺𝑇)
5 simp2r 1198 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
6 cdlemi.b . . . . . 6 𝐵 = (Base‘𝐾)
7 cdlemi.l . . . . . 6 = (le‘𝐾)
8 cdlemi.j . . . . . 6 = (join‘𝐾)
9 cdlemi.m . . . . . 6 = (meet‘𝐾)
10 cdlemi.a . . . . . 6 𝐴 = (Atoms‘𝐾)
11 cdlemi.h . . . . . 6 𝐻 = (LHyp‘𝐾)
12 cdlemi.t . . . . . 6 𝑇 = ((LTrn‘𝐾)‘𝑊)
13 cdlemi.r . . . . . 6 𝑅 = ((trL‘𝐾)‘𝑊)
14 cdlemi.e . . . . . 6 𝐸 = ((TEndo‘𝐾)‘𝑊)
156, 7, 8, 9, 10, 11, 12, 13, 14cdlemi1 38379 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑈𝐺)‘𝑃) (𝑃 (𝑅𝐺)))
161, 2, 3, 4, 5, 15syl221anc 1379 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐺)‘𝑃) (𝑃 (𝑅𝐺)))
17 simp12 1202 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝐹𝑇)
186, 7, 8, 9, 10, 11, 12, 13, 14cdlemi2 38380 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑈𝐺)‘𝑃) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))))
191, 2, 3, 17, 4, 5, 18syl231anc 1388 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐺)‘𝑃) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))))
201hllatd 36925 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝐾 ∈ Lat)
21 simp11 1201 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2211, 12, 14tendocl 38328 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝐺𝑇) → (𝑈𝐺) ∈ 𝑇)
2321, 3, 4, 22syl3anc 1369 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (𝑈𝐺) ∈ 𝑇)
24 simp2rl 1240 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝑃𝐴)
256, 10atbase 36850 . . . . . . 7 (𝑃𝐴𝑃𝐵)
2624, 25syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝑃𝐵)
276, 11, 12ltrncl 37686 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐺) ∈ 𝑇𝑃𝐵) → ((𝑈𝐺)‘𝑃) ∈ 𝐵)
2821, 23, 26, 27syl3anc 1369 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐺)‘𝑃) ∈ 𝐵)
296, 11, 12, 13trlcl 37725 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇) → (𝑅𝐺) ∈ 𝐵)
3021, 4, 29syl2anc 588 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (𝑅𝐺) ∈ 𝐵)
316, 8latjcl 17712 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑃𝐵 ∧ (𝑅𝐺) ∈ 𝐵) → (𝑃 (𝑅𝐺)) ∈ 𝐵)
3220, 26, 30, 31syl3anc 1369 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (𝑃 (𝑅𝐺)) ∈ 𝐵)
3311, 12, 14tendocl 38328 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑈𝐸𝐹𝑇) → (𝑈𝐹) ∈ 𝑇)
3421, 3, 17, 33syl3anc 1369 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (𝑈𝐹) ∈ 𝑇)
356, 11, 12ltrncl 37686 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐹) ∈ 𝑇𝑃𝐵) → ((𝑈𝐹)‘𝑃) ∈ 𝐵)
3621, 34, 26, 35syl3anc 1369 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐹)‘𝑃) ∈ 𝐵)
3711, 12ltrncnv 37707 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → 𝐹𝑇)
3821, 17, 37syl2anc 588 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝐹𝑇)
3911, 12ltrnco 38280 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇𝐹𝑇) → (𝐺𝐹) ∈ 𝑇)
4021, 4, 38, 39syl3anc 1369 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (𝐺𝐹) ∈ 𝑇)
416, 11, 12, 13trlcl 37725 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐺𝐹) ∈ 𝑇) → (𝑅‘(𝐺𝐹)) ∈ 𝐵)
4221, 40, 41syl2anc 588 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (𝑅‘(𝐺𝐹)) ∈ 𝐵)
436, 8latjcl 17712 . . . . . 6 ((𝐾 ∈ Lat ∧ ((𝑈𝐹)‘𝑃) ∈ 𝐵 ∧ (𝑅‘(𝐺𝐹)) ∈ 𝐵) → (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))) ∈ 𝐵)
4420, 36, 42, 43syl3anc 1369 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))) ∈ 𝐵)
456, 7, 9latlem12 17739 . . . . 5 ((𝐾 ∈ Lat ∧ (((𝑈𝐺)‘𝑃) ∈ 𝐵 ∧ (𝑃 (𝑅𝐺)) ∈ 𝐵 ∧ (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))) ∈ 𝐵)) → ((((𝑈𝐺)‘𝑃) (𝑃 (𝑅𝐺)) ∧ ((𝑈𝐺)‘𝑃) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) ↔ ((𝑈𝐺)‘𝑃) ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))))))
4620, 28, 32, 44, 45syl13anc 1370 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((((𝑈𝐺)‘𝑃) (𝑃 (𝑅𝐺)) ∧ ((𝑈𝐺)‘𝑃) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) ↔ ((𝑈𝐺)‘𝑃) ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))))))
4716, 19, 46mpbi2and 712 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐺)‘𝑃) ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))))
48 hlatl 36921 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
491, 48syl 17 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → 𝐾 ∈ AtLat)
507, 10, 11, 12ltrnat 37701 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐺) ∈ 𝑇𝑃𝐴) → ((𝑈𝐺)‘𝑃) ∈ 𝐴)
5121, 23, 24, 50syl3anc 1369 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐺)‘𝑃) ∈ 𝐴)
527, 10, 11, 12ltrnel 37700 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐹) ∈ 𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝑈𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈𝐹)‘𝑃) 𝑊))
5321, 34, 5, 52syl3anc 1369 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (((𝑈𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈𝐹)‘𝑃) 𝑊))
546, 7, 8, 9, 10, 11, 12, 13, 14cdlemi1 38379 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐸𝐹𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑈𝐹)‘𝑃) (𝑃 (𝑅𝐹)))
551, 2, 3, 17, 5, 54syl221anc 1379 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐹)‘𝑃) (𝑃 (𝑅𝐹)))
565, 53, 553jca 1126 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (((𝑈𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈𝐹)‘𝑃) 𝑊) ∧ ((𝑈𝐹)‘𝑃) (𝑃 (𝑅𝐹))))
57 eqid 2759 . . . . . . 7 ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) = ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))))
586, 7, 8, 9, 10, 11, 12, 13, 57cdlemh 38378 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (((𝑈𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈𝐹)‘𝑃) 𝑊) ∧ ((𝑈𝐹)‘𝑃) (𝑃 (𝑅𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) ∈ 𝐴 ∧ ¬ ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) 𝑊))
5958simpld 499 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (((𝑈𝐹)‘𝑃) ∈ 𝐴 ∧ ¬ ((𝑈𝐹)‘𝑃) 𝑊) ∧ ((𝑈𝐹)‘𝑃) (𝑃 (𝑅𝐹))) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) ∈ 𝐴)
6056, 59syld3an2 1409 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) ∈ 𝐴)
617, 10atcmp 36872 . . . 4 ((𝐾 ∈ AtLat ∧ ((𝑈𝐺)‘𝑃) ∈ 𝐴 ∧ ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) ∈ 𝐴) → (((𝑈𝐺)‘𝑃) ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) ↔ ((𝑈𝐺)‘𝑃) = ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))))))
6249, 51, 60, 61syl3anc 1369 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → (((𝑈𝐺)‘𝑃) ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))) ↔ ((𝑈𝐺)‘𝑃) = ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))))))
6347, 62mpbid 235 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐺)‘𝑃) = ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹)))))
64 cdlemi.s . 2 𝑆 = ((𝑃 (𝑅𝐺)) (((𝑈𝐹)‘𝑃) (𝑅‘(𝐺𝐹))))
6563, 64eqtr4di 2812 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) ∧ (𝑈𝐸 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ (𝑅𝐹) ≠ (𝑅𝐺))) → ((𝑈𝐺)‘𝑃) = 𝑆)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112   ≠ wne 2949   class class class wbr 5025   I cid 5422  ◡ccnv 5516   ↾ cres 5519   ∘ ccom 5521  ‘cfv 6328  (class class class)co 7143  Basecbs 16526  lecple 16615  joincjn 17605  meetcmee 17606  Latclat 17706  Atomscatm 36824  AtLatcal 36825  HLchlt 36911  LHypclh 37545  LTrncltrn 37662  trLctrl 37719  TEndoctendo 38313 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pow 5227  ax-pr 5291  ax-un 7452  ax-riotaBAD 36514 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-ral 3073  df-rex 3074  df-reu 3075  df-rmo 3076  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-pw 4489  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-iun 4878  df-iin 4879  df-br 5026  df-opab 5088  df-mpt 5106  df-id 5423  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7101  df-ov 7146  df-oprab 7147  df-mpo 7148  df-1st 7686  df-2nd 7687  df-undef 7942  df-map 8411  df-proset 17589  df-poset 17607  df-plt 17619  df-lub 17635  df-glb 17636  df-join 17637  df-meet 17638  df-p0 17700  df-p1 17701  df-lat 17707  df-clat 17769  df-oposet 36737  df-ol 36739  df-oml 36740  df-covers 36827  df-ats 36828  df-atl 36859  df-cvlat 36883  df-hlat 36912  df-llines 37059  df-lplanes 37060  df-lvols 37061  df-lines 37062  df-psubsp 37064  df-pmap 37065  df-padd 37357  df-lhyp 37549  df-laut 37550  df-ldil 37665  df-ltrn 37666  df-trl 37720  df-tendo 38316 This theorem is referenced by:  cdlemj1  38382
 Copyright terms: Public domain W3C validator