Step | Hyp | Ref
| Expression |
1 | | atcvr0eq.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
2 | | atcvr0eq.c |
. . . . . 6
β’ πΆ = ( β βπΎ) |
3 | | atcvr0eq.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
4 | 1, 2, 3 | atcvr1 37926 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) |
5 | | atcvr0eq.z |
. . . . . . . 8
β’ 0 =
(0.βπΎ) |
6 | 5, 2, 3 | atcvr0 37796 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄) β 0 πΆπ) |
7 | 6 | 3adant3 1133 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β 0 πΆπ) |
8 | 7 | biantrurd 534 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (ππΆ(π β¨ π) β ( 0 πΆπ β§ ππΆ(π β¨ π)))) |
9 | 4, 8 | bitrd 279 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β ( 0 πΆπ β§ ππΆ(π β¨ π)))) |
10 | | simp1 1137 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β πΎ β HL) |
11 | | hlop 37870 |
. . . . . . 7
β’ (πΎ β HL β πΎ β OP) |
12 | 11 | 3ad2ant1 1134 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β πΎ β OP) |
13 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
14 | 13, 5 | op0cl 37692 |
. . . . . 6
β’ (πΎ β OP β 0 β
(BaseβπΎ)) |
15 | 12, 14 | syl 17 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β 0 β (BaseβπΎ)) |
16 | 13, 3 | atbase 37797 |
. . . . . 6
β’ (π β π΄ β π β (BaseβπΎ)) |
17 | 16 | 3ad2ant2 1135 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β (BaseβπΎ)) |
18 | 13, 1, 3 | hlatjcl 37875 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
19 | 13, 2 | cvrntr 37934 |
. . . . 5
β’ ((πΎ β HL β§ ( 0 β
(BaseβπΎ) β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β (( 0 πΆπ β§ ππΆ(π β¨ π)) β Β¬ 0 πΆ(π β¨ π))) |
20 | 10, 15, 17, 18, 19 | syl13anc 1373 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (( 0 πΆπ β§ ππΆ(π β¨ π)) β Β¬ 0 πΆ(π β¨ π))) |
21 | 9, 20 | sylbid 239 |
. . 3
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β Β¬ 0 πΆ(π β¨ π))) |
22 | 21 | necon4ad 2959 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( 0 πΆ(π β¨ π) β π = π)) |
23 | 1, 3 | hlatjidm 37877 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
24 | 23 | 3adant3 1133 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = π) |
25 | 7, 24 | breqtrrd 5134 |
. . 3
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β 0 πΆ(π β¨ π)) |
26 | | oveq2 7366 |
. . . 4
β’ (π = π β (π β¨ π) = (π β¨ π)) |
27 | 26 | breq2d 5118 |
. . 3
β’ (π = π β ( 0 πΆ(π β¨ π) β 0 πΆ(π β¨ π))) |
28 | 25, 27 | syl5ibcom 244 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π = π β 0 πΆ(π β¨ π))) |
29 | 22, 28 | impbid 211 |
1
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( 0 πΆ(π β¨ π) β π = π)) |