Step | Hyp | Ref
| Expression |
1 | | atcvreq0.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
2 | | eqid 2733 |
. . . . . . . 8
β’
(leβπΎ) =
(leβπΎ) |
3 | | atcvreq0.z |
. . . . . . . 8
β’ 0 =
(0.βπΎ) |
4 | 1, 2, 3 | atl0le 37812 |
. . . . . . 7
β’ ((πΎ β AtLat β§ π β π΅) β 0 (leβπΎ)π) |
5 | 4 | 3adant3 1133 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β 0 (leβπΎ)π) |
6 | 5 | adantr 482 |
. . . . 5
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β 0 (leβπΎ)π) |
7 | | atcvreq0.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
8 | 1, 7 | atbase 37797 |
. . . . . 6
β’ (π β π΄ β π β π΅) |
9 | | eqid 2733 |
. . . . . . 7
β’
(ltβπΎ) =
(ltβπΎ) |
10 | | atcvreq0.c |
. . . . . . 7
β’ πΆ = ( β βπΎ) |
11 | 1, 9, 10 | cvrlt 37778 |
. . . . . 6
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΅) β§ ππΆπ) β π(ltβπΎ)π) |
12 | 8, 11 | syl3anl3 1415 |
. . . . 5
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β π(ltβπΎ)π) |
13 | | atlpos 37809 |
. . . . . . . 8
β’ (πΎ β AtLat β πΎ β Poset) |
14 | 13 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β πΎ β Poset) |
15 | 14 | adantr 482 |
. . . . . 6
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β πΎ β Poset) |
16 | 1, 3 | atl0cl 37811 |
. . . . . . . 8
β’ (πΎ β AtLat β 0 β π΅) |
17 | 16 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β 0 β π΅) |
18 | 17 | adantr 482 |
. . . . . 6
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β 0 β π΅) |
19 | 8 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β π β π΅) |
20 | 19 | adantr 482 |
. . . . . 6
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β π β π΅) |
21 | | simpl2 1193 |
. . . . . 6
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β π β π΅) |
22 | 3, 10, 7 | atcvr0 37796 |
. . . . . . . 8
β’ ((πΎ β AtLat β§ π β π΄) β 0 πΆπ) |
23 | 22 | 3adant2 1132 |
. . . . . . 7
β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β 0 πΆπ) |
24 | 23 | adantr 482 |
. . . . . 6
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β 0 πΆπ) |
25 | 1, 2, 9, 10 | cvrnbtwn3 37784 |
. . . . . 6
β’ ((πΎ β Poset β§ ( 0 β π΅ β§ π β π΅ β§ π β π΅) β§ 0 πΆπ) β (( 0 (leβπΎ)π β§ π(ltβπΎ)π) β 0 = π)) |
26 | 15, 18, 20, 21, 24, 25 | syl131anc 1384 |
. . . . 5
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β (( 0 (leβπΎ)π β§ π(ltβπΎ)π) β 0 = π)) |
27 | 6, 12, 26 | mpbi2and 711 |
. . . 4
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β 0 = π) |
28 | 27 | eqcomd 2739 |
. . 3
β’ (((πΎ β AtLat β§ π β π΅ β§ π β π΄) β§ ππΆπ) β π = 0 ) |
29 | 28 | ex 414 |
. 2
β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β (ππΆπ β π = 0 )) |
30 | | breq1 5109 |
. . 3
β’ (π = 0 β (ππΆπ β 0 πΆπ)) |
31 | 23, 30 | syl5ibrcom 247 |
. 2
β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β (π = 0 β ππΆπ)) |
32 | 29, 31 | impbid 211 |
1
β’ ((πΎ β AtLat β§ π β π΅ β§ π β π΄) β (ππΆπ β π = 0 )) |