Step | Hyp | Ref
| Expression |
1 | | simpll1 1212 |
. . 3
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β πΎ β HL) |
2 | | simpll3 1214 |
. . 3
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β π β π΅) |
3 | | simpr 485 |
. . 3
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β π β π) |
4 | | simplr 767 |
. . 3
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β ππΆπ) |
5 | | lplncvrlvol.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
6 | | lplncvrlvol.c |
. . . 4
β’ πΆ = ( β βπΎ) |
7 | | lplncvrlvol.p |
. . . 4
β’ π = (LPlanesβπΎ) |
8 | | lplncvrlvol.v |
. . . 4
β’ π = (LVolsβπΎ) |
9 | 5, 6, 7, 8 | lvoli 38434 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π) β§ ππΆπ) β π β π) |
10 | 1, 2, 3, 4, 9 | syl31anc 1373 |
. 2
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β π β π) |
11 | | simpll1 1212 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β πΎ β HL) |
12 | | simpll2 1213 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β π β π΅) |
13 | 11 | hllatd 38222 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β πΎ β Lat) |
14 | | simpll3 1214 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β π β π΅) |
15 | | eqid 2732 |
. . . . . . . 8
β’
(leβπΎ) =
(leβπΎ) |
16 | 5, 15 | latref 18390 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅) β π(leβπΎ)π) |
17 | 13, 14, 16 | syl2anc 584 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β π(leβπΎ)π) |
18 | 11 | adantr 481 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β§ π β (AtomsβπΎ)) β πΎ β HL) |
19 | | simplr 767 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β§ π β (AtomsβπΎ)) β π β π) |
20 | | simpr 485 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β§ π β (AtomsβπΎ)) β π β (AtomsβπΎ)) |
21 | | eqid 2732 |
. . . . . . . . 9
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
22 | 15, 21, 8 | lvolnleat 38442 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π β§ π β (AtomsβπΎ)) β Β¬ π(leβπΎ)π) |
23 | 18, 19, 20, 22 | syl3anc 1371 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β§ π β (AtomsβπΎ)) β Β¬ π(leβπΎ)π) |
24 | 23 | ex 413 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β (π β (AtomsβπΎ) β Β¬ π(leβπΎ)π)) |
25 | 17, 24 | mt2d 136 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β Β¬ π β (AtomsβπΎ)) |
26 | | simplr 767 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β ππΆπ) |
27 | | breq1 5150 |
. . . . . . . 8
β’ (π = (0.βπΎ) β (ππΆπ β (0.βπΎ)πΆπ)) |
28 | 26, 27 | syl5ibcom 244 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β (π = (0.βπΎ) β (0.βπΎ)πΆπ)) |
29 | | eqid 2732 |
. . . . . . . . 9
β’
(0.βπΎ) =
(0.βπΎ) |
30 | 5, 29, 6, 21 | isat2 38145 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΅) β (π β (AtomsβπΎ) β (0.βπΎ)πΆπ)) |
31 | 11, 14, 30 | syl2anc 584 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β (π β (AtomsβπΎ) β (0.βπΎ)πΆπ)) |
32 | 28, 31 | sylibrd 258 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β (π = (0.βπΎ) β π β (AtomsβπΎ))) |
33 | 32 | necon3bd 2954 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β (Β¬ π β (AtomsβπΎ) β π β (0.βπΎ))) |
34 | 25, 33 | mpd 15 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β π β (0.βπΎ)) |
35 | | eqid 2732 |
. . . . . . 7
β’
(LLinesβπΎ) =
(LLinesβπΎ) |
36 | 35, 8 | lvolnelln 38448 |
. . . . . 6
β’ ((πΎ β HL β§ π β π) β Β¬ π β (LLinesβπΎ)) |
37 | 11, 36 | sylancom 588 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β Β¬ π β (LLinesβπΎ)) |
38 | 11 | adantr 481 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β§ π β (AtomsβπΎ)) β πΎ β HL) |
39 | 14 | adantr 481 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β§ π β (AtomsβπΎ)) β π β π΅) |
40 | | simpr 485 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β§ π β (AtomsβπΎ)) β π β (AtomsβπΎ)) |
41 | | simpllr 774 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β§ π β (AtomsβπΎ)) β ππΆπ) |
42 | 5, 6, 21, 35 | llni 38367 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β (AtomsβπΎ)) β§ ππΆπ) β π β (LLinesβπΎ)) |
43 | 38, 39, 40, 41, 42 | syl31anc 1373 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β§ π β (AtomsβπΎ)) β π β (LLinesβπΎ)) |
44 | 37, 43 | mtand 814 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β Β¬ π β (AtomsβπΎ)) |
45 | 7, 8 | lvolnelpln 38449 |
. . . . . 6
β’ ((πΎ β HL β§ π β π) β Β¬ π β π) |
46 | 11, 45 | sylancom 588 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β Β¬ π β π) |
47 | 5, 6, 35, 7 | llncvrlpln 38417 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π β (LLinesβπΎ) β π β π)) |
48 | 47 | adantr 481 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β (π β (LLinesβπΎ) β π β π)) |
49 | 46, 48 | mtbird 324 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β Β¬ π β (LLinesβπΎ)) |
50 | 5, 15, 29, 21, 35, 7 | lplnle 38399 |
. . . 4
β’ (((πΎ β HL β§ π β π΅) β§ (π β (0.βπΎ) β§ Β¬ π β (AtomsβπΎ) β§ Β¬ π β (LLinesβπΎ))) β βπ§ β π π§(leβπΎ)π) |
51 | 11, 12, 34, 44, 49, 50 | syl23anc 1377 |
. . 3
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β βπ§ β π π§(leβπΎ)π) |
52 | | simpr3 1196 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π§(leβπΎ)π) |
53 | | simpll1 1212 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β πΎ β HL) |
54 | | hlop 38220 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β OP) |
55 | 53, 54 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β πΎ β OP) |
56 | | simpr2 1195 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π§ β π) |
57 | 5, 7 | lplnbase 38393 |
. . . . . . . . . 10
β’ (π§ β π β π§ β π΅) |
58 | 56, 57 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π§ β π΅) |
59 | | simpll2 1213 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π β π΅) |
60 | | simpll3 1214 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π β π΅) |
61 | | simpr1 1194 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π β π) |
62 | 5, 15, 6 | cvrle 38136 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π(leβπΎ)π) |
63 | 62 | adantr 481 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π(leβπΎ)π) |
64 | | hlpos 38224 |
. . . . . . . . . . . . 13
β’ (πΎ β HL β πΎ β Poset) |
65 | 53, 64 | syl 17 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β πΎ β Poset) |
66 | 5, 15 | postr 18269 |
. . . . . . . . . . . 12
β’ ((πΎ β Poset β§ (π§ β π΅ β§ π β π΅ β§ π β π΅)) β ((π§(leβπΎ)π β§ π(leβπΎ)π) β π§(leβπΎ)π)) |
67 | 65, 58, 59, 60, 66 | syl13anc 1372 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β ((π§(leβπΎ)π β§ π(leβπΎ)π) β π§(leβπΎ)π)) |
68 | 52, 63, 67 | mp2and 697 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π§(leβπΎ)π) |
69 | 15, 6, 7, 8 | lplncvrlvol2 38474 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π§ β π β§ π β π) β§ π§(leβπΎ)π) β π§πΆπ) |
70 | 53, 56, 61, 68, 69 | syl31anc 1373 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π§πΆπ) |
71 | | simplr 767 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β ππΆπ) |
72 | 5, 15, 6 | cvrcmp2 38142 |
. . . . . . . . 9
β’ ((πΎ β OP β§ (π§ β π΅ β§ π β π΅ β§ π β π΅) β§ (π§πΆπ β§ ππΆπ)) β (π§(leβπΎ)π β π§ = π)) |
73 | 55, 58, 59, 60, 70, 71, 72 | syl132anc 1388 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β (π§(leβπΎ)π β π§ = π)) |
74 | 52, 73 | mpbid 231 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π§ = π) |
75 | 74, 56 | eqeltrrd 2834 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ (π β π β§ π§ β π β§ π§(leβπΎ)π)) β π β π) |
76 | 75 | 3exp2 1354 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π β π β (π§ β π β (π§(leβπΎ)π β π β π)))) |
77 | 76 | imp 407 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β (π§ β π β (π§(leβπΎ)π β π β π))) |
78 | 77 | rexlimdv 3153 |
. . 3
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β (βπ§ β π π§(leβπΎ)π β π β π)) |
79 | 51, 78 | mpd 15 |
. 2
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β§ π β π) β π β π) |
80 | 10, 79 | impbida 799 |
1
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π β π β π β π)) |