Step | Hyp | Ref
| Expression |
1 | | oveq1 7369 |
. . . . . . . 8
β’ (π = π
β (π β¨ π
) = (π
β¨ π
)) |
2 | | islpln2a.j |
. . . . . . . . . 10
β’ β¨ =
(joinβπΎ) |
3 | | islpln2a.a |
. . . . . . . . . 10
β’ π΄ = (AtomsβπΎ) |
4 | 2, 3 | hlatjidm 37860 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π
β π΄) β (π
β¨ π
) = π
) |
5 | 4 | 3ad2antr2 1190 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (π
β¨ π
) = π
) |
6 | 1, 5 | sylan9eqr 2799 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β§ π = π
) β (π β¨ π
) = π
) |
7 | 6 | oveq1d 7377 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β§ π = π
) β ((π β¨ π
) β¨ π) = (π
β¨ π)) |
8 | | simpll 766 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β§ π = π
) β πΎ β HL) |
9 | | simplr2 1217 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β§ π = π
) β π
β π΄) |
10 | | simplr3 1218 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β§ π = π
) β π β π΄) |
11 | | islpln2a.p |
. . . . . . . 8
β’ π = (LPlanesβπΎ) |
12 | 2, 3, 11 | 2atnelpln 38036 |
. . . . . . 7
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β Β¬ (π
β¨ π) β π) |
13 | 8, 9, 10, 12 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β§ π = π
) β Β¬ (π
β¨ π) β π) |
14 | 7, 13 | eqneltrd 2858 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β§ π = π
) β Β¬ ((π β¨ π
) β¨ π) β π) |
15 | 14 | ex 414 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (π = π
β Β¬ ((π β¨ π
) β¨ π) β π)) |
16 | 15 | necon2ad 2959 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (((π β¨ π
) β¨ π) β π β π β π
)) |
17 | | hllat 37854 |
. . . . . . 7
β’ (πΎ β HL β πΎ β Lat) |
18 | 17 | adantr 482 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β πΎ β Lat) |
19 | | simpr3 1197 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β π β π΄) |
20 | | eqid 2737 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
21 | 20, 3 | atbase 37780 |
. . . . . . 7
β’ (π β π΄ β π β (BaseβπΎ)) |
22 | 19, 21 | syl 17 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
23 | 20, 2, 3 | hlatjcl 37858 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π
β π΄) β (π β¨ π
) β (BaseβπΎ)) |
24 | 23 | 3adant3r3 1185 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (π β¨ π
) β (BaseβπΎ)) |
25 | | islpln2a.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
26 | 20, 25, 2 | latleeqj2 18348 |
. . . . . 6
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ)) β (π β€ (π β¨ π
) β ((π β¨ π
) β¨ π) = (π β¨ π
))) |
27 | 18, 22, 24, 26 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (π β€ (π β¨ π
) β ((π β¨ π
) β¨ π) = (π β¨ π
))) |
28 | 2, 3, 11 | 2atnelpln 38036 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π
β π΄) β Β¬ (π β¨ π
) β π) |
29 | 28 | 3adant3r3 1185 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β Β¬ (π β¨ π
) β π) |
30 | | eleq1 2826 |
. . . . . . 7
β’ (((π β¨ π
) β¨ π) = (π β¨ π
) β (((π β¨ π
) β¨ π) β π β (π β¨ π
) β π)) |
31 | 30 | notbid 318 |
. . . . . 6
β’ (((π β¨ π
) β¨ π) = (π β¨ π
) β (Β¬ ((π β¨ π
) β¨ π) β π β Β¬ (π β¨ π
) β π)) |
32 | 29, 31 | syl5ibrcom 247 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (((π β¨ π
) β¨ π) = (π β¨ π
) β Β¬ ((π β¨ π
) β¨ π) β π)) |
33 | 27, 32 | sylbid 239 |
. . . 4
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (π β€ (π β¨ π
) β Β¬ ((π β¨ π
) β¨ π) β π)) |
34 | 33 | con2d 134 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (((π β¨ π
) β¨ π) β π β Β¬ π β€ (π β¨ π
))) |
35 | 16, 34 | jcad 514 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (((π β¨ π
) β¨ π) β π β (π β π
β§ Β¬ π β€ (π β¨ π
)))) |
36 | 25, 2, 3, 11 | lplni2 38029 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄) β§ (π β π
β§ Β¬ π β€ (π β¨ π
))) β ((π β¨ π
) β¨ π) β π) |
37 | 36 | 3expia 1122 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β ((π β π
β§ Β¬ π β€ (π β¨ π
)) β ((π β¨ π
) β¨ π) β π)) |
38 | 35, 37 | impbid 211 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β (((π β¨ π
) β¨ π) β π β (π β π
β§ Β¬ π β€ (π β¨ π
)))) |