Step | Hyp | Ref
| Expression |
1 | | isat3.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | isat3.z |
. . . 4
β’ 0 =
(0.βπΎ) |
3 | | eqid 2733 |
. . . 4
β’ ( β
βπΎ) = ( β
βπΎ) |
4 | | isat3.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
5 | 1, 2, 3, 4 | isat 37794 |
. . 3
β’ (πΎ β AtLat β (π β π΄ β (π β π΅ β§ 0 ( β βπΎ)π))) |
6 | | simpl 484 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΅) β πΎ β AtLat) |
7 | 1, 2 | atl0cl 37811 |
. . . . . . 7
β’ (πΎ β AtLat β 0 β π΅) |
8 | 7 | adantr 482 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΅) β 0 β π΅) |
9 | | simpr 486 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΅) β π β π΅) |
10 | | isat3.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
11 | | eqid 2733 |
. . . . . . 7
β’
(ltβπΎ) =
(ltβπΎ) |
12 | 1, 10, 11, 3 | cvrval2 37782 |
. . . . . 6
β’ ((πΎ β AtLat β§ 0 β π΅ β§ π β π΅) β ( 0 ( β βπΎ)π β ( 0 (ltβπΎ)π β§ βπ₯ β π΅ (( 0 (ltβπΎ)π₯ β§ π₯ β€ π) β π₯ = π)))) |
13 | 6, 8, 9, 12 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β AtLat β§ π β π΅) β ( 0 ( β βπΎ)π β ( 0 (ltβπΎ)π β§ βπ₯ β π΅ (( 0 (ltβπΎ)π₯ β§ π₯ β€ π) β π₯ = π)))) |
14 | 1, 11, 2 | atlltn0 37814 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΅) β ( 0 (ltβπΎ)π β π β 0 )) |
15 | 1, 11, 2 | atlltn0 37814 |
. . . . . . . . . . 11
β’ ((πΎ β AtLat β§ π₯ β π΅) β ( 0 (ltβπΎ)π₯ β π₯ β 0 )) |
16 | 15 | adantlr 714 |
. . . . . . . . . 10
β’ (((πΎ β AtLat β§ π β π΅) β§ π₯ β π΅) β ( 0 (ltβπΎ)π₯ β π₯ β 0 )) |
17 | 16 | imbi1d 342 |
. . . . . . . . 9
β’ (((πΎ β AtLat β§ π β π΅) β§ π₯ β π΅) β (( 0 (ltβπΎ)π₯ β π₯ = π) β (π₯ β 0 β π₯ = π))) |
18 | 17 | imbi2d 341 |
. . . . . . . 8
β’ (((πΎ β AtLat β§ π β π΅) β§ π₯ β π΅) β ((π₯ β€ π β ( 0 (ltβπΎ)π₯ β π₯ = π)) β (π₯ β€ π β (π₯ β 0 β π₯ = π)))) |
19 | | impexp 452 |
. . . . . . . . 9
β’ ((( 0
(ltβπΎ)π₯ β§ π₯ β€ π) β π₯ = π) β ( 0 (ltβπΎ)π₯ β (π₯ β€ π β π₯ = π))) |
20 | | bi2.04 389 |
. . . . . . . . 9
β’ (( 0
(ltβπΎ)π₯ β (π₯ β€ π β π₯ = π)) β (π₯ β€ π β ( 0 (ltβπΎ)π₯ β π₯ = π))) |
21 | 19, 20 | bitri 275 |
. . . . . . . 8
β’ ((( 0
(ltβπΎ)π₯ β§ π₯ β€ π) β π₯ = π) β (π₯ β€ π β ( 0 (ltβπΎ)π₯ β π₯ = π))) |
22 | | orcom 869 |
. . . . . . . . . 10
β’ ((π₯ = π β¨ π₯ = 0 ) β (π₯ = 0 β¨ π₯ = π)) |
23 | | neor 3033 |
. . . . . . . . . 10
β’ ((π₯ = 0 β¨ π₯ = π) β (π₯ β 0 β π₯ = π)) |
24 | 22, 23 | bitri 275 |
. . . . . . . . 9
β’ ((π₯ = π β¨ π₯ = 0 ) β (π₯ β 0 β π₯ = π)) |
25 | 24 | imbi2i 336 |
. . . . . . . 8
β’ ((π₯ β€ π β (π₯ = π β¨ π₯ = 0 )) β (π₯ β€ π β (π₯ β 0 β π₯ = π))) |
26 | 18, 21, 25 | 3bitr4g 314 |
. . . . . . 7
β’ (((πΎ β AtLat β§ π β π΅) β§ π₯ β π΅) β ((( 0 (ltβπΎ)π₯ β§ π₯ β€ π) β π₯ = π) β (π₯ β€ π β (π₯ = π β¨ π₯ = 0 )))) |
27 | 26 | ralbidva 3169 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΅) β (βπ₯ β π΅ (( 0 (ltβπΎ)π₯ β§ π₯ β€ π) β π₯ = π) β βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 )))) |
28 | 14, 27 | anbi12d 632 |
. . . . 5
β’ ((πΎ β AtLat β§ π β π΅) β (( 0 (ltβπΎ)π β§ βπ₯ β π΅ (( 0 (ltβπΎ)π₯ β§ π₯ β€ π) β π₯ = π)) β (π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 ))))) |
29 | 13, 28 | bitr2d 280 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΅) β ((π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 ))) β 0 ( β
βπΎ)π)) |
30 | 29 | pm5.32da 580 |
. . 3
β’ (πΎ β AtLat β ((π β π΅ β§ (π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 )))) β (π β π΅ β§ 0 ( β βπΎ)π))) |
31 | 5, 30 | bitr4d 282 |
. 2
β’ (πΎ β AtLat β (π β π΄ β (π β π΅ β§ (π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 )))))) |
32 | | 3anass 1096 |
. 2
β’ ((π β π΅ β§ π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 ))) β (π β π΅ β§ (π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 ))))) |
33 | 31, 32 | bitr4di 289 |
1
β’ (πΎ β AtLat β (π β π΄ β (π β π΅ β§ π β 0 β§ βπ₯ β π΅ (π₯ β€ π β (π₯ = π β¨ π₯ = 0 ))))) |