Step | Hyp | Ref
| Expression |
1 | | oveq1 7369 |
. . . . . . . . 9
β’ (π = π β (π β¨ π) = (π β¨ π)) |
2 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β πΎ β HL) |
3 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π β π΄) |
4 | | islvol2a.j |
. . . . . . . . . . 11
β’ β¨ =
(joinβπΎ) |
5 | | islvol2a.a |
. . . . . . . . . . 11
β’ π΄ = (AtomsβπΎ) |
6 | 4, 5 | hlatjidm 37860 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
7 | 2, 3, 6 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π β¨ π) = π) |
8 | 1, 7 | sylan9eqr 2799 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β (π β¨ π) = π) |
9 | 8 | oveq1d 7377 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β ((π β¨ π) β¨ π
) = (π β¨ π
)) |
10 | 9 | oveq1d 7377 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β (((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π
) β¨ π)) |
11 | | simprl 770 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π
β π΄) |
12 | | simprr 772 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π β π΄) |
13 | | islvol2a.v |
. . . . . . . . 9
β’ π = (LVolsβπΎ) |
14 | 4, 5, 13 | 3atnelvolN 38078 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β Β¬ ((π β¨ π
) β¨ π) β π) |
15 | 2, 3, 11, 12, 14 | syl13anc 1373 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β Β¬ ((π β¨ π
) β¨ π) β π) |
16 | 15 | adantr 482 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β Β¬ ((π β¨ π
) β¨ π) β π) |
17 | 10, 16 | eqneltrd 2858 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π) |
18 | 17 | ex 414 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π = π β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
19 | 18 | necon2ad 2959 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β π β π)) |
20 | 2 | hllatd 37855 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β πΎ β Lat) |
21 | | eqid 2737 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
22 | 21, 5 | atbase 37780 |
. . . . . . 7
β’ (π
β π΄ β π
β (BaseβπΎ)) |
23 | 22 | ad2antrl 727 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π
β (BaseβπΎ)) |
24 | 21, 4, 5 | hlatjcl 37858 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
25 | 24 | adantr 482 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
26 | | islvol2a.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
27 | 21, 26, 4 | latleeqj2 18348 |
. . . . . 6
β’ ((πΎ β Lat β§ π
β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β (π
β€ (π β¨ π) β ((π β¨ π) β¨ π
) = (π β¨ π))) |
28 | 20, 23, 25, 27 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π
β€ (π β¨ π) β ((π β¨ π) β¨ π
) = (π β¨ π))) |
29 | | simpl2 1193 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π β π΄) |
30 | 4, 5, 13 | 3atnelvolN 38078 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β Β¬ ((π β¨ π) β¨ π) β π) |
31 | 2, 29, 3, 12, 30 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β Β¬ ((π β¨ π) β¨ π) β π) |
32 | | oveq1 7369 |
. . . . . . . 8
β’ (((π β¨ π) β¨ π
) = (π β¨ π) β (((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π)) |
33 | 32 | eleq1d 2823 |
. . . . . . 7
β’ (((π β¨ π) β¨ π
) = (π β¨ π) β ((((π β¨ π) β¨ π
) β¨ π) β π β ((π β¨ π) β¨ π) β π)) |
34 | 33 | notbid 318 |
. . . . . 6
β’ (((π β¨ π) β¨ π
) = (π β¨ π) β (Β¬ (((π β¨ π) β¨ π
) β¨ π) β π β Β¬ ((π β¨ π) β¨ π) β π)) |
35 | 31, 34 | syl5ibrcom 247 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π
) = (π β¨ π) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
36 | 28, 35 | sylbid 239 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π
β€ (π β¨ π) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
37 | 36 | con2d 134 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β Β¬ π
β€ (π β¨ π))) |
38 | 21, 5 | atbase 37780 |
. . . . . . 7
β’ (π β π΄ β π β (BaseβπΎ)) |
39 | 38 | ad2antll 728 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
40 | 21, 4 | latjcl 18335 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π
β (BaseβπΎ)) β ((π β¨ π) β¨ π
) β (BaseβπΎ)) |
41 | 20, 25, 23, 40 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π
) β (BaseβπΎ)) |
42 | 21, 26, 4 | latleeqj2 18348 |
. . . . . 6
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ ((π β¨ π) β¨ π
) β (BaseβπΎ)) β (π β€ ((π β¨ π) β¨ π
) β (((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
))) |
43 | 20, 39, 41, 42 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π β€ ((π β¨ π) β¨ π
) β (((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
))) |
44 | 4, 5, 13 | 3atnelvolN 38078 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β Β¬ ((π β¨ π) β¨ π
) β π) |
45 | 2, 29, 3, 11, 44 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β Β¬ ((π β¨ π) β¨ π
) β π) |
46 | | eleq1 2826 |
. . . . . . 7
β’ ((((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
) β ((((π β¨ π) β¨ π
) β¨ π) β π β ((π β¨ π) β¨ π
) β π)) |
47 | 46 | notbid 318 |
. . . . . 6
β’ ((((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
) β (Β¬ (((π β¨ π) β¨ π
) β¨ π) β π β Β¬ ((π β¨ π) β¨ π
) β π)) |
48 | 45, 47 | syl5ibrcom 247 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
49 | 43, 48 | sylbid 239 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π β€ ((π β¨ π) β¨ π
) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
50 | 49 | con2d 134 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β Β¬ π β€ ((π β¨ π) β¨ π
))) |
51 | 19, 37, 50 | 3jcad 1130 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β (π β π β§ Β¬ π
β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π
)))) |
52 | 26, 4, 5, 13 | lvoli2 38073 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π
β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π
))) β (((π β¨ π) β¨ π
) β¨ π) β π) |
53 | 52 | 3expia 1122 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((π β π β§ Β¬ π
β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π
)) β (((π β¨ π) β¨ π
) β¨ π) β π)) |
54 | 51, 53 | impbid 211 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β (π β π β§ Β¬ π
β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π
)))) |