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

Theorem cdleme5 35028
Description: Part of proof of Lemma E in [Crawley] p. 113. 𝐺 represents fs(r). We show r fs(r)) = p q at the top of p. 114. (Contributed by NM, 7-Jun-2012.)
Hypotheses
Ref Expression
cdleme4.l = (le‘𝐾)
cdleme4.j = (join‘𝐾)
cdleme4.m = (meet‘𝐾)
cdleme4.a 𝐴 = (Atoms‘𝐾)
cdleme4.h 𝐻 = (LHyp‘𝐾)
cdleme4.u 𝑈 = ((𝑃 𝑄) 𝑊)
cdleme4.f 𝐹 = ((𝑆 𝑈) (𝑄 ((𝑃 𝑆) 𝑊)))
cdleme4.g 𝐺 = ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊)))
Assertion
Ref Expression
cdleme5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 𝐺) = (𝑃 𝑄))

Proof of Theorem cdleme5
StepHypRef Expression
1 cdleme4.g . . 3 𝐺 = ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊)))
21oveq2i 6618 . 2 (𝑅 𝐺) = (𝑅 ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊))))
3 simp1l 1083 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝐾 ∈ HL)
4 simp23l 1180 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑅𝐴)
5 simp21 1092 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑃𝐴)
6 simp22 1093 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑄𝐴)
7 eqid 2621 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
8 cdleme4.j . . . . . 6 = (join‘𝐾)
9 cdleme4.a . . . . . 6 𝐴 = (Atoms‘𝐾)
107, 8, 9hlatjcl 34154 . . . . 5 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
113, 5, 6, 10syl3anc 1323 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑃 𝑄) ∈ (Base‘𝐾))
12 hllat 34151 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ Lat)
133, 12syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝐾 ∈ Lat)
14 simp1 1059 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
15 simp3ll 1130 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑆𝐴)
16 cdleme4.l . . . . . . 7 = (le‘𝐾)
17 cdleme4.m . . . . . . 7 = (meet‘𝐾)
18 cdleme4.h . . . . . . 7 𝐻 = (LHyp‘𝐾)
19 cdleme4.u . . . . . . 7 𝑈 = ((𝑃 𝑄) 𝑊)
20 cdleme4.f . . . . . . 7 𝐹 = ((𝑆 𝑈) (𝑄 ((𝑃 𝑆) 𝑊)))
2116, 8, 17, 9, 18, 19, 20, 7cdleme1b 35014 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴𝑆𝐴)) → 𝐹 ∈ (Base‘𝐾))
2214, 5, 6, 15, 21syl13anc 1325 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝐹 ∈ (Base‘𝐾))
237, 8, 9hlatjcl 34154 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) → (𝑅 𝑆) ∈ (Base‘𝐾))
243, 4, 15, 23syl3anc 1323 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 𝑆) ∈ (Base‘𝐾))
25 simp1r 1084 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑊𝐻)
267, 18lhpbase 34785 . . . . . . 7 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2725, 26syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑊 ∈ (Base‘𝐾))
287, 17latmcl 16976 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑅 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑅 𝑆) 𝑊) ∈ (Base‘𝐾))
2913, 24, 27, 28syl3anc 1323 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → ((𝑅 𝑆) 𝑊) ∈ (Base‘𝐾))
307, 8latjcl 16975 . . . . 5 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑅 𝑆) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑅 𝑆) 𝑊)) ∈ (Base‘𝐾))
3113, 22, 29, 30syl3anc 1323 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝐹 ((𝑅 𝑆) 𝑊)) ∈ (Base‘𝐾))
32 simp3r 1088 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑅 (𝑃 𝑄))
337, 16, 8, 17, 9atmod3i1 34651 . . . 4 ((𝐾 ∈ HL ∧ (𝑅𝐴 ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑅 𝑆) 𝑊)) ∈ (Base‘𝐾)) ∧ 𝑅 (𝑃 𝑄)) → (𝑅 ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊)))) = ((𝑃 𝑄) (𝑅 (𝐹 ((𝑅 𝑆) 𝑊)))))
343, 4, 11, 31, 32, 33syl131anc 1336 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊)))) = ((𝑃 𝑄) (𝑅 (𝐹 ((𝑅 𝑆) 𝑊)))))
357, 9atbase 34077 . . . . . . 7 (𝑆𝐴𝑆 ∈ (Base‘𝐾))
3615, 35syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑆 ∈ (Base‘𝐾))
377, 16, 8latlej2 16985 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑆 ∈ (Base‘𝐾) ∧ (𝑃 𝑄) ∈ (Base‘𝐾)) → (𝑃 𝑄) (𝑆 (𝑃 𝑄)))
3813, 36, 11, 37syl3anc 1323 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑃 𝑄) (𝑆 (𝑃 𝑄)))
397, 9atbase 34077 . . . . . . . . 9 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
404, 39syl 17 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑅 ∈ (Base‘𝐾))
417, 8latj12 17020 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑅 ∈ (Base‘𝐾) ∧ 𝐹 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾))) → (𝑅 (𝐹 𝑆)) = (𝐹 (𝑅 𝑆)))
4213, 40, 22, 36, 41syl13anc 1325 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 (𝐹 𝑆)) = (𝐹 (𝑅 𝑆)))
4316, 8, 17, 9, 18, 19, 7cdleme0aa 34998 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑃𝐴𝑄𝐴) → 𝑈 ∈ (Base‘𝐾))
4414, 5, 6, 43syl3anc 1323 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑈 ∈ (Base‘𝐾))
457, 8latj12 17020 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑆 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾))) → (𝑆 (𝑅 𝑈)) = (𝑅 (𝑆 𝑈)))
4613, 36, 40, 44, 45syl13anc 1325 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑆 (𝑅 𝑈)) = (𝑅 (𝑆 𝑈)))
4716, 8, 17, 9, 18, 19cdleme4 35026 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝑅 (𝑃 𝑄)) → (𝑃 𝑄) = (𝑅 𝑈))
48473adant3l 1319 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑃 𝑄) = (𝑅 𝑈))
4948oveq2d 6623 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑆 (𝑃 𝑄)) = (𝑆 (𝑅 𝑈)))
507, 8latjcom 16983 . . . . . . . . . . 11 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ 𝑆 ∈ (Base‘𝐾)) → (𝐹 𝑆) = (𝑆 𝐹))
5113, 22, 36, 50syl3anc 1323 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝐹 𝑆) = (𝑆 𝐹))
52 simp3l 1087 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑆𝐴 ∧ ¬ 𝑆 𝑊))
5316, 8, 17, 9, 18, 19, 20cdleme1 35015 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊))) → (𝑆 𝐹) = (𝑆 𝑈))
5414, 5, 6, 52, 53syl13anc 1325 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑆 𝐹) = (𝑆 𝑈))
5551, 54eqtrd 2655 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝐹 𝑆) = (𝑆 𝑈))
5655oveq2d 6623 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 (𝐹 𝑆)) = (𝑅 (𝑆 𝑈)))
5746, 49, 563eqtr4d 2665 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑆 (𝑃 𝑄)) = (𝑅 (𝐹 𝑆)))
5816, 8, 9hlatlej1 34162 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) → 𝑅 (𝑅 𝑆))
593, 4, 15, 58syl3anc 1323 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝑅 (𝑅 𝑆))
607, 16, 8, 17, 9atmod3i1 34651 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ (𝑅𝐴 ∧ (𝑅 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) ∧ 𝑅 (𝑅 𝑆)) → (𝑅 ((𝑅 𝑆) 𝑊)) = ((𝑅 𝑆) (𝑅 𝑊)))
613, 4, 24, 27, 59, 60syl131anc 1336 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 ((𝑅 𝑆) 𝑊)) = ((𝑅 𝑆) (𝑅 𝑊)))
62 simp23r 1181 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → ¬ 𝑅 𝑊)
63 eqid 2621 . . . . . . . . . . . . 13 (1.‘𝐾) = (1.‘𝐾)
6416, 8, 63, 9, 18lhpjat2 34808 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) → (𝑅 𝑊) = (1.‘𝐾))
6514, 4, 62, 64syl12anc 1321 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 𝑊) = (1.‘𝐾))
6665oveq2d 6623 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → ((𝑅 𝑆) (𝑅 𝑊)) = ((𝑅 𝑆) (1.‘𝐾)))
67 hlol 34149 . . . . . . . . . . . 12 (𝐾 ∈ HL → 𝐾 ∈ OL)
683, 67syl 17 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → 𝐾 ∈ OL)
697, 17, 63olm11 34015 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ (𝑅 𝑆) ∈ (Base‘𝐾)) → ((𝑅 𝑆) (1.‘𝐾)) = (𝑅 𝑆))
7068, 24, 69syl2anc 692 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → ((𝑅 𝑆) (1.‘𝐾)) = (𝑅 𝑆))
7166, 70eqtrd 2655 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → ((𝑅 𝑆) (𝑅 𝑊)) = (𝑅 𝑆))
7261, 71eqtrd 2655 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 ((𝑅 𝑆) 𝑊)) = (𝑅 𝑆))
7372oveq2d 6623 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝐹 (𝑅 ((𝑅 𝑆) 𝑊))) = (𝐹 (𝑅 𝑆)))
7442, 57, 733eqtr4d 2665 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑆 (𝑃 𝑄)) = (𝐹 (𝑅 ((𝑅 𝑆) 𝑊))))
757, 8latj12 17020 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝐹 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾) ∧ ((𝑅 𝑆) 𝑊) ∈ (Base‘𝐾))) → (𝐹 (𝑅 ((𝑅 𝑆) 𝑊))) = (𝑅 (𝐹 ((𝑅 𝑆) 𝑊))))
7613, 22, 40, 29, 75syl13anc 1325 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝐹 (𝑅 ((𝑅 𝑆) 𝑊))) = (𝑅 (𝐹 ((𝑅 𝑆) 𝑊))))
7774, 76eqtrd 2655 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑆 (𝑃 𝑄)) = (𝑅 (𝐹 ((𝑅 𝑆) 𝑊))))
7838, 77breqtrd 4641 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑃 𝑄) (𝑅 (𝐹 ((𝑅 𝑆) 𝑊))))
797, 8latjcl 16975 . . . . . 6 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝐹 ((𝑅 𝑆) 𝑊)) ∈ (Base‘𝐾)) → (𝑅 (𝐹 ((𝑅 𝑆) 𝑊))) ∈ (Base‘𝐾))
8013, 40, 31, 79syl3anc 1323 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 (𝐹 ((𝑅 𝑆) 𝑊))) ∈ (Base‘𝐾))
817, 16, 17latleeqm1 17003 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝑅 (𝐹 ((𝑅 𝑆) 𝑊))) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝑅 (𝐹 ((𝑅 𝑆) 𝑊))) ↔ ((𝑃 𝑄) (𝑅 (𝐹 ((𝑅 𝑆) 𝑊)))) = (𝑃 𝑄)))
8213, 11, 80, 81syl3anc 1323 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → ((𝑃 𝑄) (𝑅 (𝐹 ((𝑅 𝑆) 𝑊))) ↔ ((𝑃 𝑄) (𝑅 (𝐹 ((𝑅 𝑆) 𝑊)))) = (𝑃 𝑄)))
8378, 82mpbid 222 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → ((𝑃 𝑄) (𝑅 (𝐹 ((𝑅 𝑆) 𝑊)))) = (𝑃 𝑄))
8434, 83eqtrd 2655 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊)))) = (𝑃 𝑄))
852, 84syl5eq 2667 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 𝐺) = (𝑃 𝑄))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987   class class class wbr 4615  cfv 5849  (class class class)co 6607  Basecbs 15784  lecple 15872  joincjn 16868  meetcmee 16869  1.cp1 16962  Latclat 16969  OLcol 33962  Atomscatm 34051  HLchlt 34138  LHypclh 34771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-1st 7116  df-2nd 7117  df-preset 16852  df-poset 16870  df-plt 16882  df-lub 16898  df-glb 16899  df-join 16900  df-meet 16901  df-p0 16963  df-p1 16964  df-lat 16970  df-clat 17032  df-oposet 33964  df-ol 33966  df-oml 33967  df-covers 34054  df-ats 34055  df-atl 34086  df-cvlat 34110  df-hlat 34139  df-psubsp 34290  df-pmap 34291  df-padd 34583  df-lhyp 34775
This theorem is referenced by:  cdleme6  35029  cdleme7e  35035  cdleme18b  35080  cdleme50trn2a  35339
  Copyright terms: Public domain W3C validator