Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
2 | | simpl3 1194 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
3 | | simpr 486 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β π) |
4 | | eqidd 2738 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (π β¨ π) = (π β¨ π)) |
5 | | neeq1 3007 |
. . . . 5
β’ (π = π β (π β π β π β π )) |
6 | | oveq1 7369 |
. . . . . 6
β’ (π = π β (π β¨ π ) = (π β¨ π )) |
7 | 6 | eqeq2d 2748 |
. . . . 5
β’ (π = π β ((π β¨ π) = (π β¨ π ) β (π β¨ π) = (π β¨ π ))) |
8 | 5, 7 | anbi12d 632 |
. . . 4
β’ (π = π β ((π β π β§ (π β¨ π) = (π β¨ π )) β (π β π β§ (π β¨ π) = (π β¨ π )))) |
9 | | neeq2 3008 |
. . . . 5
β’ (π = π β (π β π β π β π)) |
10 | | oveq2 7370 |
. . . . . 6
β’ (π = π β (π β¨ π ) = (π β¨ π)) |
11 | 10 | eqeq2d 2748 |
. . . . 5
β’ (π = π β ((π β¨ π) = (π β¨ π ) β (π β¨ π) = (π β¨ π))) |
12 | 9, 11 | anbi12d 632 |
. . . 4
β’ (π = π β ((π β π β§ (π β¨ π) = (π β¨ π )) β (π β π β§ (π β¨ π) = (π β¨ π)))) |
13 | 8, 12 | rspc2ev 3595 |
. . 3
β’ ((π β π΄ β§ π β π΄ β§ (π β π β§ (π β¨ π) = (π β¨ π))) β βπ β π΄ βπ β π΄ (π β π β§ (π β¨ π) = (π β¨ π ))) |
14 | 1, 2, 3, 4, 13 | syl112anc 1375 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β βπ β π΄ βπ β π΄ (π β π β§ (π β¨ π) = (π β¨ π ))) |
15 | | simpl1 1192 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β πΎ β HL) |
16 | | eqid 2737 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
17 | | llni2.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
18 | | llni2.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
19 | 16, 17, 18 | hlatjcl 37858 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
20 | 19 | adantr 482 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (π β¨ π) β (BaseβπΎ)) |
21 | | llni2.n |
. . . 4
β’ π = (LLinesβπΎ) |
22 | 16, 17, 18, 21 | islln3 38002 |
. . 3
β’ ((πΎ β HL β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β π β βπ β π΄ βπ β π΄ (π β π β§ (π β¨ π) = (π β¨ π )))) |
23 | 15, 20, 22 | syl2anc 585 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π) β π β βπ β π΄ βπ β π΄ (π β π β§ (π β¨ π) = (π β¨ π )))) |
24 | 14, 23 | mpbird 257 |
1
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (π β¨ π) β π) |