Step | Hyp | Ref
| Expression |
1 | | simp3 1139 |
. . 3
β’ ((πΎ β HL β§ π β π β§ π β π) β π β π) |
2 | | eqid 2733 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
3 | | eqid 2733 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
4 | | eqid 2733 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
5 | | lplnnlelln.n |
. . . . 5
β’ π = (LLinesβπΎ) |
6 | 2, 3, 4, 5 | islln2 38382 |
. . . 4
β’ (πΎ β HL β (π β π β (π β (BaseβπΎ) β§ βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = (π(joinβπΎ)π))))) |
7 | 6 | 3ad2ant1 1134 |
. . 3
β’ ((πΎ β HL β§ π β π β§ π β π) β (π β π β (π β (BaseβπΎ) β§ βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = (π(joinβπΎ)π))))) |
8 | 1, 7 | mpbid 231 |
. 2
β’ ((πΎ β HL β§ π β π β§ π β π) β (π β (BaseβπΎ) β§ βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = (π(joinβπΎ)π)))) |
9 | | simp11 1204 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π))) β πΎ β HL) |
10 | | simp12 1205 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π))) β π β π) |
11 | | simp2l 1200 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π))) β π β (AtomsβπΎ)) |
12 | | simp2r 1201 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π))) β π β (AtomsβπΎ)) |
13 | | lplnnlelln.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
14 | | lplnnlelln.p |
. . . . . . . 8
β’ π = (LPlanesβπΎ) |
15 | 13, 3, 4, 14 | lplnnle2at 38412 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β Β¬ π β€ (π(joinβπΎ)π)) |
16 | 9, 10, 11, 12, 15 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π))) β Β¬ π β€ (π(joinβπΎ)π)) |
17 | | simp3r 1203 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π))) β π = (π(joinβπΎ)π)) |
18 | 17 | breq2d 5161 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π))) β (π β€ π β π β€ (π(joinβπΎ)π))) |
19 | 16, 18 | mtbird 325 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (π β π β§ π = (π(joinβπΎ)π))) β Β¬ π β€ π) |
20 | 19 | 3exp 1120 |
. . . 4
β’ ((πΎ β HL β§ π β π β§ π β π) β ((π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β ((π β π β§ π = (π(joinβπΎ)π)) β Β¬ π β€ π))) |
21 | 20 | rexlimdvv 3211 |
. . 3
β’ ((πΎ β HL β§ π β π β§ π β π) β (βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = (π(joinβπΎ)π)) β Β¬ π β€ π)) |
22 | 21 | adantld 492 |
. 2
β’ ((πΎ β HL β§ π β π β§ π β π) β ((π β (BaseβπΎ) β§ βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = (π(joinβπΎ)π))) β Β¬ π β€ π)) |
23 | 8, 22 | mpd 15 |
1
β’ ((πΎ β HL β§ π β π β§ π β π) β Β¬ π β€ π) |