Step | Hyp | Ref
| Expression |
1 | | simpr1 1195 |
. . . 4
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄)) β π β π) |
2 | | eqid 2737 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
3 | | eqid 2737 |
. . . . . 6
β’ ( β
βπΎ) = ( β
βπΎ) |
4 | | eqid 2737 |
. . . . . 6
β’
(LLinesβπΎ) =
(LLinesβπΎ) |
5 | | lplnnle2at.p |
. . . . . 6
β’ π = (LPlanesβπΎ) |
6 | 2, 3, 4, 5 | islpln 38022 |
. . . . 5
β’ (πΎ β HL β (π β π β (π β (BaseβπΎ) β§ βπ¦ β (LLinesβπΎ)π¦( β βπΎ)π))) |
7 | 6 | adantr 482 |
. . . 4
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄)) β (π β π β (π β (BaseβπΎ) β§ βπ¦ β (LLinesβπΎ)π¦( β βπΎ)π))) |
8 | 1, 7 | mpbid 231 |
. . 3
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄)) β (π β (BaseβπΎ) β§ βπ¦ β (LLinesβπΎ)π¦( β βπΎ)π)) |
9 | 8 | simprd 497 |
. 2
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄)) β βπ¦ β (LLinesβπΎ)π¦( β βπΎ)π) |
10 | | oveq1 7369 |
. . . . . . . . 9
β’ (π = π
β (π β¨ π
) = (π
β¨ π
)) |
11 | 10 | breq2d 5122 |
. . . . . . . 8
β’ (π = π
β (π β€ (π β¨ π
) β π β€ (π
β¨ π
))) |
12 | 11 | notbid 318 |
. . . . . . 7
β’ (π = π
β (Β¬ π β€ (π β¨ π
) β Β¬ π β€ (π
β¨ π
))) |
13 | | simpl1 1192 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β πΎ β HL) |
14 | | simpl3l 1229 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β π¦ β (LLinesβπΎ)) |
15 | | simpl22 1253 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β π β π΄) |
16 | | simpl23 1254 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β π
β π΄) |
17 | | simpr 486 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β π β π
) |
18 | | lplnnle2at.j |
. . . . . . . . . . 11
β’ β¨ =
(joinβπΎ) |
19 | | lplnnle2at.a |
. . . . . . . . . . 11
β’ π΄ = (AtomsβπΎ) |
20 | 18, 19, 4 | llni2 38004 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΄ β§ π
β π΄) β§ π β π
) β (π β¨ π
) β (LLinesβπΎ)) |
21 | 13, 15, 16, 17, 20 | syl31anc 1374 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β (π β¨ π
) β (LLinesβπΎ)) |
22 | | eqid 2737 |
. . . . . . . . . 10
β’
(ltβπΎ) =
(ltβπΎ) |
23 | 22, 4 | llnnlt 38015 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π¦ β (LLinesβπΎ) β§ (π β¨ π
) β (LLinesβπΎ)) β Β¬ π¦(ltβπΎ)(π β¨ π
)) |
24 | 13, 14, 21, 23 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β Β¬ π¦(ltβπΎ)(π β¨ π
)) |
25 | 2, 4 | llnbase 38001 |
. . . . . . . . . . 11
β’ (π¦ β (LLinesβπΎ) β π¦ β (BaseβπΎ)) |
26 | 14, 25 | syl 17 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β π¦ β (BaseβπΎ)) |
27 | | simpl21 1252 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β π β π) |
28 | 2, 5 | lplnbase 38026 |
. . . . . . . . . . 11
β’ (π β π β π β (BaseβπΎ)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β π β (BaseβπΎ)) |
30 | | simpl3r 1230 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β π¦( β βπΎ)π) |
31 | 2, 22, 3 | cvrlt 37761 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π¦ β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ π¦( β βπΎ)π) β π¦(ltβπΎ)π) |
32 | 13, 26, 29, 30, 31 | syl31anc 1374 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β π¦(ltβπΎ)π) |
33 | | hlpos 37857 |
. . . . . . . . . . 11
β’ (πΎ β HL β πΎ β Poset) |
34 | 13, 33 | syl 17 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β πΎ β Poset) |
35 | 2, 18, 19 | hlatjcl 37858 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β π΄ β§ π
β π΄) β (π β¨ π
) β (BaseβπΎ)) |
36 | 13, 15, 16, 35 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β (π β¨ π
) β (BaseβπΎ)) |
37 | | lplnnle2at.l |
. . . . . . . . . . 11
β’ β€ =
(leβπΎ) |
38 | 2, 37, 22 | pltletr 18239 |
. . . . . . . . . 10
β’ ((πΎ β Poset β§ (π¦ β (BaseβπΎ) β§ π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ))) β ((π¦(ltβπΎ)π β§ π β€ (π β¨ π
)) β π¦(ltβπΎ)(π β¨ π
))) |
39 | 34, 26, 29, 36, 38 | syl13anc 1373 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β ((π¦(ltβπΎ)π β§ π β€ (π β¨ π
)) β π¦(ltβπΎ)(π β¨ π
))) |
40 | 32, 39 | mpand 694 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β (π β€ (π β¨ π
) β π¦(ltβπΎ)(π β¨ π
))) |
41 | 24, 40 | mtod 197 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β§ π β π
) β Β¬ π β€ (π β¨ π
)) |
42 | | simp1 1137 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β πΎ β HL) |
43 | | simp3l 1202 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β π¦ β (LLinesβπΎ)) |
44 | | simp23 1209 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β π
β π΄) |
45 | 37, 19, 4 | llnnleat 38005 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π¦ β (LLinesβπΎ) β§ π
β π΄) β Β¬ π¦ β€ π
) |
46 | 42, 43, 44, 45 | syl3anc 1372 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β Β¬ π¦ β€ π
) |
47 | 43, 25 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β π¦ β (BaseβπΎ)) |
48 | | simp21 1207 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β π β π) |
49 | 48, 28 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β π β (BaseβπΎ)) |
50 | | simp3r 1203 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β π¦( β βπΎ)π) |
51 | 42, 47, 49, 50, 31 | syl31anc 1374 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β π¦(ltβπΎ)π) |
52 | 33 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β πΎ β Poset) |
53 | 2, 19 | atbase 37780 |
. . . . . . . . . . . . 13
β’ (π
β π΄ β π
β (BaseβπΎ)) |
54 | 44, 53 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β π
β (BaseβπΎ)) |
55 | 2, 37, 22 | pltletr 18239 |
. . . . . . . . . . . 12
β’ ((πΎ β Poset β§ (π¦ β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π
β (BaseβπΎ))) β ((π¦(ltβπΎ)π β§ π β€ π
) β π¦(ltβπΎ)π
)) |
56 | 52, 47, 49, 54, 55 | syl13anc 1373 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β ((π¦(ltβπΎ)π β§ π β€ π
) β π¦(ltβπΎ)π
)) |
57 | 51, 56 | mpand 694 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β (π β€ π
β π¦(ltβπΎ)π
)) |
58 | 37, 22 | pltle 18229 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π¦ β (LLinesβπΎ) β§ π
β π΄) β (π¦(ltβπΎ)π
β π¦ β€ π
)) |
59 | 42, 43, 44, 58 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β (π¦(ltβπΎ)π
β π¦ β€ π
)) |
60 | 57, 59 | syld 47 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β (π β€ π
β π¦ β€ π
)) |
61 | 46, 60 | mtod 197 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β Β¬ π β€ π
) |
62 | 18, 19 | hlatjidm 37860 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π
β π΄) β (π
β¨ π
) = π
) |
63 | 42, 44, 62 | syl2anc 585 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β (π
β¨ π
) = π
) |
64 | 63 | breq2d 5122 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β (π β€ (π
β¨ π
) β π β€ π
)) |
65 | 61, 64 | mtbird 325 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β Β¬ π β€ (π
β¨ π
)) |
66 | 12, 41, 65 | pm2.61ne 3031 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄) β§ (π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π)) β Β¬ π β€ (π β¨ π
)) |
67 | 66 | 3exp 1120 |
. . . . 5
β’ (πΎ β HL β ((π β π β§ π β π΄ β§ π
β π΄) β ((π¦ β (LLinesβπΎ) β§ π¦( β βπΎ)π) β Β¬ π β€ (π β¨ π
)))) |
68 | 67 | exp4a 433 |
. . . 4
β’ (πΎ β HL β ((π β π β§ π β π΄ β§ π
β π΄) β (π¦ β (LLinesβπΎ) β (π¦( β βπΎ)π β Β¬ π β€ (π β¨ π
))))) |
69 | 68 | imp 408 |
. . 3
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄)) β (π¦ β (LLinesβπΎ) β (π¦( β βπΎ)π β Β¬ π β€ (π β¨ π
)))) |
70 | 69 | rexlimdv 3151 |
. 2
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄)) β (βπ¦ β (LLinesβπΎ)π¦( β βπΎ)π β Β¬ π β€ (π β¨ π
))) |
71 | 9, 70 | mpd 15 |
1
β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π
β π΄)) β Β¬ π β€ (π β¨ π
)) |