Step | Hyp | Ref
| Expression |
1 | | oveq1 7412 |
. . . . . . . . 9
β’ (π = π β (π β¨ π) = (π β¨ π)) |
2 | | simpl1 1188 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β πΎ β HL) |
3 | | simpl3 1190 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π β π΄) |
4 | | islvol2a.j |
. . . . . . . . . . 11
β’ β¨ =
(joinβπΎ) |
5 | | islvol2a.a |
. . . . . . . . . . 11
β’ π΄ = (AtomsβπΎ) |
6 | 4, 5 | hlatjidm 38752 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
7 | 2, 3, 6 | syl2anc 583 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π β¨ π) = π) |
8 | 1, 7 | sylan9eqr 2788 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β (π β¨ π) = π) |
9 | 8 | oveq1d 7420 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β ((π β¨ π) β¨ π
) = (π β¨ π
)) |
10 | 9 | oveq1d 7420 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β (((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π
) β¨ π)) |
11 | | simprl 768 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π
β π΄) |
12 | | simprr 770 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π β π΄) |
13 | | islvol2a.v |
. . . . . . . . 9
β’ π = (LVolsβπΎ) |
14 | 4, 5, 13 | 3atnelvolN 38970 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄)) β Β¬ ((π β¨ π
) β¨ π) β π) |
15 | 2, 3, 11, 12, 14 | syl13anc 1369 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β Β¬ ((π β¨ π
) β¨ π) β π) |
16 | 15 | adantr 480 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β Β¬ ((π β¨ π
) β¨ π) β π) |
17 | 10, 16 | eqneltrd 2847 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β§ π = π) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π) |
18 | 17 | ex 412 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π = π β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
19 | 18 | necon2ad 2949 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β π β π)) |
20 | 2 | hllatd 38747 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β πΎ β Lat) |
21 | | eqid 2726 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
22 | 21, 5 | atbase 38672 |
. . . . . . 7
β’ (π
β π΄ β π
β (BaseβπΎ)) |
23 | 22 | ad2antrl 725 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π
β (BaseβπΎ)) |
24 | 21, 4, 5 | hlatjcl 38750 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
25 | 24 | adantr 480 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
26 | | islvol2a.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
27 | 21, 26, 4 | latleeqj2 18417 |
. . . . . 6
β’ ((πΎ β Lat β§ π
β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β (π
β€ (π β¨ π) β ((π β¨ π) β¨ π
) = (π β¨ π))) |
28 | 20, 23, 25, 27 | syl3anc 1368 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π
β€ (π β¨ π) β ((π β¨ π) β¨ π
) = (π β¨ π))) |
29 | | simpl2 1189 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π β π΄) |
30 | 4, 5, 13 | 3atnelvolN 38970 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β Β¬ ((π β¨ π) β¨ π) β π) |
31 | 2, 29, 3, 12, 30 | syl13anc 1369 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β Β¬ ((π β¨ π) β¨ π) β π) |
32 | | oveq1 7412 |
. . . . . . . 8
β’ (((π β¨ π) β¨ π
) = (π β¨ π) β (((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π)) |
33 | 32 | eleq1d 2812 |
. . . . . . 7
β’ (((π β¨ π) β¨ π
) = (π β¨ π) β ((((π β¨ π) β¨ π
) β¨ π) β π β ((π β¨ π) β¨ π) β π)) |
34 | 33 | notbid 318 |
. . . . . 6
β’ (((π β¨ π) β¨ π
) = (π β¨ π) β (Β¬ (((π β¨ π) β¨ π
) β¨ π) β π β Β¬ ((π β¨ π) β¨ π) β π)) |
35 | 31, 34 | syl5ibrcom 246 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π
) = (π β¨ π) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
36 | 28, 35 | sylbid 239 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π
β€ (π β¨ π) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
37 | 36 | con2d 134 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β Β¬ π
β€ (π β¨ π))) |
38 | 21, 5 | atbase 38672 |
. . . . . . 7
β’ (π β π΄ β π β (BaseβπΎ)) |
39 | 38 | ad2antll 726 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
40 | 21, 4 | latjcl 18404 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π
β (BaseβπΎ)) β ((π β¨ π) β¨ π
) β (BaseβπΎ)) |
41 | 20, 25, 23, 40 | syl3anc 1368 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π
) β (BaseβπΎ)) |
42 | 21, 26, 4 | latleeqj2 18417 |
. . . . . 6
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ ((π β¨ π) β¨ π
) β (BaseβπΎ)) β (π β€ ((π β¨ π) β¨ π
) β (((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
))) |
43 | 20, 39, 41, 42 | syl3anc 1368 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π β€ ((π β¨ π) β¨ π
) β (((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
))) |
44 | 4, 5, 13 | 3atnelvolN 38970 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β Β¬ ((π β¨ π) β¨ π
) β π) |
45 | 2, 29, 3, 11, 44 | syl13anc 1369 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β Β¬ ((π β¨ π) β¨ π
) β π) |
46 | | eleq1 2815 |
. . . . . . 7
β’ ((((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
) β ((((π β¨ π) β¨ π
) β¨ π) β π β ((π β¨ π) β¨ π
) β π)) |
47 | 46 | notbid 318 |
. . . . . 6
β’ ((((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
) β (Β¬ (((π β¨ π) β¨ π
) β¨ π) β π β Β¬ ((π β¨ π) β¨ π
) β π)) |
48 | 45, 47 | syl5ibrcom 246 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) = ((π β¨ π) β¨ π
) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
49 | 43, 48 | sylbid 239 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β (π β€ ((π β¨ π) β¨ π
) β Β¬ (((π β¨ π) β¨ π
) β¨ π) β π)) |
50 | 49 | con2d 134 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β Β¬ π β€ ((π β¨ π) β¨ π
))) |
51 | 19, 37, 50 | 3jcad 1126 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β (π β π β§ Β¬ π
β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π
)))) |
52 | 26, 4, 5, 13 | lvoli2 38965 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π
β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π
))) β (((π β¨ π) β¨ π
) β¨ π) β π) |
53 | 52 | 3expia 1118 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((π β π β§ Β¬ π
β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π
)) β (((π β¨ π) β¨ π
) β¨ π) β π)) |
54 | 51, 53 | impbid 211 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π
β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π
) β¨ π) β π β (π β π β§ Β¬ π
β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π
)))) |