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

Theorem cdlemkid1 38237
 Description: Lemma for cdlemkid 38251. (Contributed by NM, 24-Jul-2013.)
Hypotheses
Ref Expression
cdlemk5.b 𝐵 = (Base‘𝐾)
cdlemk5.l = (le‘𝐾)
cdlemk5.j = (join‘𝐾)
cdlemk5.m = (meet‘𝐾)
cdlemk5.a 𝐴 = (Atoms‘𝐾)
cdlemk5.h 𝐻 = (LHyp‘𝐾)
cdlemk5.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk5.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk5.z 𝑍 = ((𝑃 (𝑅𝑏)) ((𝑁𝑃) (𝑅‘(𝑏𝐹))))
Assertion
Ref Expression
cdlemkid1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 (𝑅𝑏)) = (𝑃 (𝑅𝑏)))

Proof of Theorem cdlemkid1
StepHypRef Expression
1 cdlemk5.z . . 3 𝑍 = ((𝑃 (𝑅𝑏)) ((𝑁𝑃) (𝑅‘(𝑏𝐹))))
21oveq1i 7146 . 2 (𝑍 (𝑅𝑏)) = (((𝑃 (𝑅𝑏)) ((𝑁𝑃) (𝑅‘(𝑏𝐹)))) (𝑅𝑏))
3 simp1l 1194 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ HL)
4 simp1 1133 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
5 simp3rl 1243 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏𝑇)
6 simp3rr 1244 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏 ≠ ( I ↾ 𝐵))
7 cdlemk5.b . . . . . 6 𝐵 = (Base‘𝐾)
8 cdlemk5.a . . . . . 6 𝐴 = (Atoms‘𝐾)
9 cdlemk5.h . . . . . 6 𝐻 = (LHyp‘𝐾)
10 cdlemk5.t . . . . . 6 𝑇 = ((LTrn‘𝐾)‘𝑊)
11 cdlemk5.r . . . . . 6 𝑅 = ((trL‘𝐾)‘𝑊)
127, 8, 9, 10, 11trlnidat 37488 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)) → (𝑅𝑏) ∈ 𝐴)
134, 5, 6, 12syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅𝑏) ∈ 𝐴)
14 simp3ll 1241 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃𝐴)
15 cdlemk5.j . . . . . 6 = (join‘𝐾)
167, 15, 8hlatjcl 36682 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝑅𝑏) ∈ 𝐴) → (𝑃 (𝑅𝑏)) ∈ 𝐵)
173, 14, 13, 16syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 (𝑅𝑏)) ∈ 𝐵)
183hllatd 36679 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ Lat)
19 simp22 1204 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑁𝑇)
207, 8atbase 36604 . . . . . . 7 (𝑃𝐴𝑃𝐵)
2114, 20syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃𝐵)
227, 9, 10ltrncl 37440 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑁𝑇𝑃𝐵) → (𝑁𝑃) ∈ 𝐵)
234, 19, 21, 22syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑁𝑃) ∈ 𝐵)
24 simp21 1203 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐹𝑇)
259, 10ltrncnv 37461 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → 𝐹𝑇)
264, 24, 25syl2anc 587 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → 𝐹𝑇)
279, 10ltrnco 38034 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑏𝑇𝐹𝑇) → (𝑏𝐹) ∈ 𝑇)
284, 5, 26, 27syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑏𝐹) ∈ 𝑇)
297, 9, 10, 11trlcl 37479 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑏𝐹) ∈ 𝑇) → (𝑅‘(𝑏𝐹)) ∈ 𝐵)
304, 28, 29syl2anc 587 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘(𝑏𝐹)) ∈ 𝐵)
317, 15latjcl 17656 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑁𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏𝐹)) ∈ 𝐵) → ((𝑁𝑃) (𝑅‘(𝑏𝐹))) ∈ 𝐵)
3218, 23, 30, 31syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁𝑃) (𝑅‘(𝑏𝐹))) ∈ 𝐵)
33 cdlemk5.l . . . . . 6 = (le‘𝐾)
3433, 15, 8hlatlej2 36691 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝑅𝑏) ∈ 𝐴) → (𝑅𝑏) (𝑃 (𝑅𝑏)))
353, 14, 13, 34syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅𝑏) (𝑃 (𝑅𝑏)))
36 cdlemk5.m . . . . 5 = (meet‘𝐾)
377, 33, 15, 36, 8atmod2i1 37176 . . . 4 ((𝐾 ∈ HL ∧ ((𝑅𝑏) ∈ 𝐴 ∧ (𝑃 (𝑅𝑏)) ∈ 𝐵 ∧ ((𝑁𝑃) (𝑅‘(𝑏𝐹))) ∈ 𝐵) ∧ (𝑅𝑏) (𝑃 (𝑅𝑏))) → (((𝑃 (𝑅𝑏)) ((𝑁𝑃) (𝑅‘(𝑏𝐹)))) (𝑅𝑏)) = ((𝑃 (𝑅𝑏)) (((𝑁𝑃) (𝑅‘(𝑏𝐹))) (𝑅𝑏))))
383, 13, 17, 32, 35, 37syl131anc 1380 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 (𝑅𝑏)) ((𝑁𝑃) (𝑅‘(𝑏𝐹)))) (𝑅𝑏)) = ((𝑃 (𝑅𝑏)) (((𝑁𝑃) (𝑅‘(𝑏𝐹))) (𝑅𝑏))))
397, 8atbase 36604 . . . . . . . 8 ((𝑅𝑏) ∈ 𝐴 → (𝑅𝑏) ∈ 𝐵)
4013, 39syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅𝑏) ∈ 𝐵)
417, 9, 10, 11trlcl 37479 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑁𝑇) → (𝑅𝑁) ∈ 𝐵)
424, 19, 41syl2anc 587 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅𝑁) ∈ 𝐵)
437, 15latj32 17702 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃𝐵 ∧ (𝑅𝑏) ∈ 𝐵 ∧ (𝑅𝑁) ∈ 𝐵)) → ((𝑃 (𝑅𝑏)) (𝑅𝑁)) = ((𝑃 (𝑅𝑁)) (𝑅𝑏)))
4418, 21, 40, 42, 43syl13anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 (𝑅𝑏)) (𝑅𝑁)) = ((𝑃 (𝑅𝑁)) (𝑅𝑏)))
45 simp3l 1198 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
4633, 15, 8, 9, 10, 11trljat3 37483 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑁𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅𝑁)) = ((𝑁𝑃) (𝑅𝑁)))
474, 19, 45, 46syl3anc 1368 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 (𝑅𝑁)) = ((𝑁𝑃) (𝑅𝑁)))
4847oveq1d 7151 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 (𝑅𝑁)) (𝑅𝑏)) = (((𝑁𝑃) (𝑅𝑁)) (𝑅𝑏)))
497, 15latjass 17700 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑁𝑃) ∈ 𝐵 ∧ (𝑅𝑁) ∈ 𝐵 ∧ (𝑅𝑏) ∈ 𝐵)) → (((𝑁𝑃) (𝑅𝑁)) (𝑅𝑏)) = ((𝑁𝑃) ((𝑅𝑁) (𝑅𝑏))))
5018, 23, 42, 40, 49syl13anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁𝑃) (𝑅𝑁)) (𝑅𝑏)) = ((𝑁𝑃) ((𝑅𝑁) (𝑅𝑏))))
5144, 48, 503eqtrd 2837 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 (𝑅𝑏)) (𝑅𝑁)) = ((𝑁𝑃) ((𝑅𝑁) (𝑅𝑏))))
527, 15latjass 17700 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((𝑁𝑃) ∈ 𝐵 ∧ (𝑅‘(𝑏𝐹)) ∈ 𝐵 ∧ (𝑅𝑏) ∈ 𝐵)) → (((𝑁𝑃) (𝑅‘(𝑏𝐹))) (𝑅𝑏)) = ((𝑁𝑃) ((𝑅‘(𝑏𝐹)) (𝑅𝑏))))
5318, 23, 30, 40, 52syl13anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁𝑃) (𝑅‘(𝑏𝐹))) (𝑅𝑏)) = ((𝑁𝑃) ((𝑅‘(𝑏𝐹)) (𝑅𝑏))))
547, 15latjcom 17664 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑅𝑁) ∈ 𝐵 ∧ (𝑅𝑏) ∈ 𝐵) → ((𝑅𝑁) (𝑅𝑏)) = ((𝑅𝑏) (𝑅𝑁)))
5518, 42, 40, 54syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅𝑁) (𝑅𝑏)) = ((𝑅𝑏) (𝑅𝑁)))
569, 10, 11trlcnv 37480 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) = (𝑅𝐹))
574, 24, 56syl2anc 587 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅𝐹) = (𝑅𝐹))
58 simp23 1205 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅𝐹) = (𝑅𝑁))
5957, 58eqtrd 2833 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅𝐹) = (𝑅𝑁))
6059oveq2d 7152 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅𝑏) (𝑅𝐹)) = ((𝑅𝑏) (𝑅𝑁)))
6155, 60eqtr4d 2836 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅𝑁) (𝑅𝑏)) = ((𝑅𝑏) (𝑅𝐹)))
6215, 9, 10, 11trljco 38055 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑏𝑇𝐹𝑇) → ((𝑅𝑏) (𝑅‘(𝑏𝐹))) = ((𝑅𝑏) (𝑅𝐹)))
634, 5, 26, 62syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅𝑏) (𝑅‘(𝑏𝐹))) = ((𝑅𝑏) (𝑅𝐹)))
647, 15latjcom 17664 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑅𝑏) ∈ 𝐵 ∧ (𝑅‘(𝑏𝐹)) ∈ 𝐵) → ((𝑅𝑏) (𝑅‘(𝑏𝐹))) = ((𝑅‘(𝑏𝐹)) (𝑅𝑏)))
6518, 40, 30, 64syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅𝑏) (𝑅‘(𝑏𝐹))) = ((𝑅‘(𝑏𝐹)) (𝑅𝑏)))
6661, 63, 653eqtr2d 2839 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑅𝑁) (𝑅𝑏)) = ((𝑅‘(𝑏𝐹)) (𝑅𝑏)))
6766oveq2d 7152 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑁𝑃) ((𝑅𝑁) (𝑅𝑏))) = ((𝑁𝑃) ((𝑅‘(𝑏𝐹)) (𝑅𝑏))))
6853, 67eqtr4d 2836 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑁𝑃) (𝑅‘(𝑏𝐹))) (𝑅𝑏)) = ((𝑁𝑃) ((𝑅𝑁) (𝑅𝑏))))
6951, 68eqtr4d 2836 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 (𝑅𝑏)) (𝑅𝑁)) = (((𝑁𝑃) (𝑅‘(𝑏𝐹))) (𝑅𝑏)))
7069oveq2d 7152 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 (𝑅𝑏)) ((𝑃 (𝑅𝑏)) (𝑅𝑁))) = ((𝑃 (𝑅𝑏)) (((𝑁𝑃) (𝑅‘(𝑏𝐹))) (𝑅𝑏))))
717, 15, 36latabs2 17693 . . . 4 ((𝐾 ∈ Lat ∧ (𝑃 (𝑅𝑏)) ∈ 𝐵 ∧ (𝑅𝑁) ∈ 𝐵) → ((𝑃 (𝑅𝑏)) ((𝑃 (𝑅𝑏)) (𝑅𝑁))) = (𝑃 (𝑅𝑏)))
7218, 17, 42, 71syl3anc 1368 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 (𝑅𝑏)) ((𝑃 (𝑅𝑏)) (𝑅𝑁))) = (𝑃 (𝑅𝑏)))
7338, 70, 723eqtr2d 2839 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (((𝑃 (𝑅𝑏)) ((𝑁𝑃) (𝑅‘(𝑏𝐹)))) (𝑅𝑏)) = (𝑃 (𝑅𝑏)))
742, 73syl5eq 2845 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑁𝑇 ∧ (𝑅𝐹) = (𝑅𝑁)) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑏𝑇𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 (𝑅𝑏)) = (𝑃 (𝑅𝑏)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987   class class class wbr 5031   I cid 5425  ◡ccnv 5519   ↾ cres 5522   ∘ ccom 5524  ‘cfv 6325  (class class class)co 7136  Basecbs 16478  lecple 16567  joincjn 17549  meetcmee 17550  Latclat 17650  Atomscatm 36578  HLchlt 36665  LHypclh 37299  LTrncltrn 37416  trLctrl 37473 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-riotaBAD 36268 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5426  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-1st 7674  df-2nd 7675  df-undef 7925  df-map 8394  df-proset 17533  df-poset 17551  df-plt 17563  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-p0 17644  df-p1 17645  df-lat 17651  df-clat 17713  df-oposet 36491  df-ol 36493  df-oml 36494  df-covers 36581  df-ats 36582  df-atl 36613  df-cvlat 36637  df-hlat 36666  df-llines 36813  df-lplanes 36814  df-lvols 36815  df-lines 36816  df-psubsp 36818  df-pmap 36819  df-padd 37111  df-lhyp 37303  df-laut 37304  df-ldil 37419  df-ltrn 37420  df-trl 37474 This theorem is referenced by:  cdlemkid2  38239
 Copyright terms: Public domain W3C validator