Proof of Theorem cdlemg11b
Step | Hyp | Ref
| Expression |
1 | | simp33 1210 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄)) |
2 | | simpl1 1190 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
3 | | simpl31 1253 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝐺 ∈ 𝑇) |
4 | | simpl2l 1225 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
5 | | cdlemg8.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
6 | | cdlemg8.j |
. . . . . . 7
⊢ ∨ =
(join‘𝐾) |
7 | | cdlemg8.m |
. . . . . . 7
⊢ ∧ =
(meet‘𝐾) |
8 | | cdlemg8.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
9 | | cdlemg8.h |
. . . . . . 7
⊢ 𝐻 = (LHyp‘𝐾) |
10 | | cdlemg8.t |
. . . . . . 7
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
11 | | cdlemg10.r |
. . . . . . 7
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
12 | 5, 6, 7, 8, 9, 10,
11 | trlval2 38173 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊)) |
13 | 2, 3, 4, 12 | syl3anc 1370 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑅‘𝐺) = ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊)) |
14 | | eqid 2740 |
. . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) |
15 | | simpl1l 1223 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝐾 ∈ HL) |
16 | 15 | hllatd 37374 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝐾 ∈ Lat) |
17 | | simp2ll 1239 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → 𝑃 ∈ 𝐴) |
18 | 17 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑃 ∈ 𝐴) |
19 | 14, 8 | atbase 37299 |
. . . . . . . . 9
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑃 ∈ (Base‘𝐾)) |
21 | 14, 9, 10 | ltrncl 38135 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑃 ∈ (Base‘𝐾)) → (𝐺‘𝑃) ∈ (Base‘𝐾)) |
22 | 2, 3, 20, 21 | syl3anc 1370 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑃) ∈ (Base‘𝐾)) |
23 | 14, 6 | latjcl 18155 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐺‘𝑃) ∈ (Base‘𝐾)) → (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾)) |
24 | 16, 20, 22, 23 | syl3anc 1370 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾)) |
25 | | simpl1r 1224 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑊 ∈ 𝐻) |
26 | 14, 9 | lhpbase 38008 |
. . . . . . . 8
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾)) |
27 | 25, 26 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑊 ∈ (Base‘𝐾)) |
28 | 14, 7 | latmcl 18156 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾)) |
29 | 16, 24, 27, 28 | syl3anc 1370 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ∈ (Base‘𝐾)) |
30 | | simpl2r 1226 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑄 ∈ 𝐴) |
31 | 14, 8 | atbase 37299 |
. . . . . . . 8
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾)) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑄 ∈ (Base‘𝐾)) |
33 | 14, 6 | latjcl 18155 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
34 | 16, 20, 32, 33 | syl3anc 1370 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) |
35 | 14, 5, 7 | latmle1 18180 |
. . . . . . 7
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ (𝐺‘𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ (𝐺‘𝑃))) |
36 | 16, 24, 27, 35 | syl3anc 1370 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ (𝐺‘𝑃))) |
37 | 14, 5, 6 | latlej1 18164 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → 𝑃 ≤ (𝑃 ∨ 𝑄)) |
38 | 16, 20, 32, 37 | syl3anc 1370 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → 𝑃 ≤ (𝑃 ∨ 𝑄)) |
39 | 14, 9, 10 | ltrncl 38135 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇 ∧ 𝑄 ∈ (Base‘𝐾)) → (𝐺‘𝑄) ∈ (Base‘𝐾)) |
40 | 2, 3, 32, 39 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑄) ∈ (Base‘𝐾)) |
41 | 14, 5, 6 | latlej1 18164 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝐺‘𝑃) ∈ (Base‘𝐾) ∧ (𝐺‘𝑄) ∈ (Base‘𝐾)) → (𝐺‘𝑃) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) |
42 | 16, 22, 40, 41 | syl3anc 1370 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑃) ≤ ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) |
43 | | simpr 485 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) |
44 | 42, 43 | breqtrrd 5107 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝐺‘𝑃) ≤ (𝑃 ∨ 𝑄)) |
45 | 14, 5, 6 | latjle12 18166 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ (𝐺‘𝑃) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))) → ((𝑃 ≤ (𝑃 ∨ 𝑄) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ 𝑄))) |
46 | 16, 20, 22, 34, 45 | syl13anc 1371 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ≤ (𝑃 ∨ 𝑄) ∧ (𝐺‘𝑃) ≤ (𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ 𝑄))) |
47 | 38, 44, 46 | mpbi2and 709 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑃 ∨ (𝐺‘𝑃)) ≤ (𝑃 ∨ 𝑄)) |
48 | 14, 5, 16, 29, 24, 34, 36, 47 | lattrd 18162 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → ((𝑃 ∨ (𝐺‘𝑃)) ∧ 𝑊) ≤ (𝑃 ∨ 𝑄)) |
49 | 13, 48 | eqbrtrd 5101 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) ∧ (𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) → (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄)) |
50 | 49 | ex 413 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑄) = ((𝐺‘𝑃) ∨ (𝐺‘𝑄)) → (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) |
51 | 50 | necon3bd 2959 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄) → (𝑃 ∨ 𝑄) ≠ ((𝐺‘𝑃) ∨ (𝐺‘𝑄)))) |
52 | 1, 51 | mpd 15 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (𝐺 ∈ 𝑇 ∧ 𝑃 ≠ 𝑄 ∧ ¬ (𝑅‘𝐺) ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∨ 𝑄) ≠ ((𝐺‘𝑃) ∨ (𝐺‘𝑄))) |