Proof of Theorem cdlemd2
Step | Hyp | Ref
| Expression |
1 | | simp3l 1089 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘𝑃) = (𝐺‘𝑃)) |
2 | | simp11 1091 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
3 | | simp12l 1174 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝐹 ∈ 𝑇) |
4 | | simp11l 1172 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝐾 ∈ HL) |
5 | | hllat 34650 |
. . . . . . . . . 10
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
6 | 4, 5 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝐾 ∈ Lat) |
7 | | simp21l 1178 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝑃 ∈ 𝐴) |
8 | | simp13 1093 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝑅 ∈ 𝐴) |
9 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Base‘𝐾) =
(Base‘𝐾) |
10 | | cdlemd2.j |
. . . . . . . . . . 11
⊢ ∨ =
(join‘𝐾) |
11 | | cdlemd2.a |
. . . . . . . . . . 11
⊢ 𝐴 = (Atoms‘𝐾) |
12 | 9, 10, 11 | hlatjcl 34653 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑃 ∨ 𝑅) ∈ (Base‘𝐾)) |
13 | 4, 7, 8, 12 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝑃 ∨ 𝑅) ∈ (Base‘𝐾)) |
14 | | simp11r 1173 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝑊 ∈ 𝐻) |
15 | | cdlemd2.h |
. . . . . . . . . . 11
⊢ 𝐻 = (LHyp‘𝐾) |
16 | 9, 15 | lhpbase 35284 |
. . . . . . . . . 10
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
17 | 14, 16 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝑊 ∈ (Base‘𝐾)) |
18 | | eqid 2622 |
. . . . . . . . . 10
⊢
(meet‘𝐾) =
(meet‘𝐾) |
19 | 9, 18 | latmcl 17052 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
20 | 6, 13, 17, 19 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
21 | | cdlemd2.l |
. . . . . . . . . 10
⊢ ≤ =
(le‘𝐾) |
22 | 9, 21, 18 | latmle2 17077 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ≤ 𝑊) |
23 | 6, 13, 17, 22 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ≤ 𝑊) |
24 | | cdlemd2.t |
. . . . . . . . 9
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
25 | 9, 21, 15, 24 | ltrnval1 35420 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ≤ 𝑊)) → (𝐹‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) = ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) |
26 | 2, 3, 20, 23, 25 | syl112anc 1330 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) = ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) |
27 | | simp12r 1175 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝐺 ∈ 𝑇) |
28 | 9, 21, 15, 24 | ltrnval1 35420 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ≤ 𝑊)) → (𝐺‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) = ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) |
29 | 2, 27, 20, 23, 28 | syl112anc 1330 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐺‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) = ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) |
30 | 26, 29 | eqtr4d 2659 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) = (𝐺‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))) |
31 | 1, 30 | oveq12d 6668 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → ((𝐹‘𝑃) ∨ (𝐹‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐺‘𝑃) ∨ (𝐺‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
32 | 9, 11 | atbase 34576 |
. . . . . . 7
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
33 | 7, 32 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝑃 ∈ (Base‘𝐾)) |
34 | 9, 10, 15, 24 | ltrnj 35418 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾))) → (𝐹‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐹‘𝑃) ∨ (𝐹‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
35 | 2, 3, 33, 20, 34 | syl112anc 1330 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐹‘𝑃) ∨ (𝐹‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
36 | 9, 10, 15, 24 | ltrnj 35418 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾))) → (𝐺‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐺‘𝑃) ∨ (𝐺‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
37 | 2, 27, 33, 20, 36 | syl112anc 1330 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐺‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐺‘𝑃) ∨ (𝐺‘((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
38 | 31, 35, 37 | 3eqtr4d 2666 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))) = (𝐺‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
39 | | simp3r 1090 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘𝑄) = (𝐺‘𝑄)) |
40 | | simp22l 1180 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝑄 ∈ 𝐴) |
41 | 9, 10, 11 | hlatjcl 34653 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) |
42 | 4, 40, 8, 41 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝑄 ∨ 𝑅) ∈ (Base‘𝐾)) |
43 | 9, 18 | latmcl 17052 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
44 | 6, 42, 17, 43 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) |
45 | 9, 21, 18 | latmle2 17077 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑅) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ≤ 𝑊) |
46 | 6, 42, 17, 45 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ≤ 𝑊) |
47 | 9, 21, 15, 24 | ltrnval1 35420 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ≤ 𝑊)) → (𝐹‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) = ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) |
48 | 2, 3, 44, 46, 47 | syl112anc 1330 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) = ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) |
49 | 9, 21, 15, 24 | ltrnval1 35420 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ≤ 𝑊)) → (𝐺‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) = ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) |
50 | 2, 27, 44, 46, 49 | syl112anc 1330 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐺‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) = ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) |
51 | 48, 50 | eqtr4d 2659 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) = (𝐺‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))) |
52 | 39, 51 | oveq12d 6668 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → ((𝐹‘𝑄) ∨ (𝐹‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐺‘𝑄) ∨ (𝐺‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
53 | 9, 11 | atbase 34576 |
. . . . . . 7
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
54 | 40, 53 | syl 17 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝑄 ∈ (Base‘𝐾)) |
55 | 9, 10, 15, 24 | ltrnj 35418 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾))) → (𝐹‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐹‘𝑄) ∨ (𝐹‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
56 | 2, 3, 54, 44, 55 | syl112anc 1330 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐹‘𝑄) ∨ (𝐹‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
57 | 9, 10, 15, 24 | ltrnj 35418 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑄 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾))) → (𝐺‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐺‘𝑄) ∨ (𝐺‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
58 | 2, 27, 54, 44, 57 | syl112anc 1330 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐺‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))) = ((𝐺‘𝑄) ∨ (𝐺‘((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
59 | 52, 56, 58 | 3eqtr4d 2666 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))) = (𝐺‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
60 | 38, 59 | oveq12d 6668 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → ((𝐹‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))(meet‘𝐾)(𝐹‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) = ((𝐺‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))(meet‘𝐾)(𝐺‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))))) |
61 | 9, 10 | latjcl 17051 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) ∈ (Base‘𝐾)) |
62 | 6, 33, 20, 61 | syl3anc 1326 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) ∈ (Base‘𝐾)) |
63 | 9, 10 | latjcl 17051 |
. . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊) ∈ (Base‘𝐾)) → (𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) ∈ (Base‘𝐾)) |
64 | 6, 54, 44, 63 | syl3anc 1326 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) ∈ (Base‘𝐾)) |
65 | 9, 18, 15, 24 | ltrnm 35417 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) ∈ (Base‘𝐾) ∧ (𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))) → (𝐹‘((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) = ((𝐹‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))(meet‘𝐾)(𝐹‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))))) |
66 | 2, 3, 62, 64, 65 | syl112anc 1330 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) = ((𝐹‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))(meet‘𝐾)(𝐹‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))))) |
67 | 9, 18, 15, 24 | ltrnm 35417 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ ((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)) ∈ (Base‘𝐾) ∧ (𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)) ∈ (Base‘𝐾))) → (𝐺‘((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) = ((𝐺‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))(meet‘𝐾)(𝐺‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))))) |
68 | 2, 27, 62, 64, 67 | syl112anc 1330 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐺‘((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) = ((𝐺‘(𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊)))(meet‘𝐾)(𝐺‘(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))))) |
69 | 60, 66, 68 | 3eqtr4d 2666 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) = (𝐺‘((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))))) |
70 | | simp21 1094 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
71 | | simp22 1095 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
72 | | simp23l 1182 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝑃 ≠ 𝑄) |
73 | | simp23r 1183 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) |
74 | 8, 72, 73 | 3jca 1242 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝑅 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) |
75 | 21, 10, 18, 11, 15 | cdlemd1 35485 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)))) → 𝑅 = ((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
76 | 2, 70, 71, 74, 75 | syl13anc 1328 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → 𝑅 = ((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊)))) |
77 | 76 | fveq2d 6195 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘𝑅) = (𝐹‘((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))))) |
78 | 76 | fveq2d 6195 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐺‘𝑅) = (𝐺‘((𝑃 ∨ ((𝑃 ∨ 𝑅)(meet‘𝐾)𝑊))(meet‘𝐾)(𝑄 ∨ ((𝑄 ∨ 𝑅)(meet‘𝐾)𝑊))))) |
79 | 69, 77, 78 | 3eqtr4d 2666 |
1
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) ∧ 𝑅 ∈ 𝐴) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝐹‘𝑃) = (𝐺‘𝑃) ∧ (𝐹‘𝑄) = (𝐺‘𝑄))) → (𝐹‘𝑅) = (𝐺‘𝑅)) |