Step | Hyp | Ref
| Expression |
1 | | lnatex.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | eqid 2732 |
. . . 4
β’
(joinβπΎ) =
(joinβπΎ) |
3 | | lnatex.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
4 | | lnatex.n |
. . . 4
β’ π = (LinesβπΎ) |
5 | | lnatex.m |
. . . 4
β’ π = (pmapβπΎ) |
6 | 1, 2, 3, 4, 5 | isline3 38642 |
. . 3
β’ ((πΎ β HL β§ π β π΅) β ((πβπ) β π β βπ β π΄ βπ β π΄ (π β π β§ π = (π(joinβπΎ)π )))) |
7 | 6 | biimp3a 1469 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β βπ β π΄ βπ β π΄ (π β π β§ π = (π(joinβπΎ)π ))) |
8 | | simpl2r 1227 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β π β π΄) |
9 | | simpl3l 1228 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β π β π ) |
10 | 9 | necomd 2996 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β π β π) |
11 | | simpr 485 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β π = π) |
12 | 10, 11 | neeqtrd 3010 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β π β π) |
13 | | simpl11 1248 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β πΎ β HL) |
14 | | simpl2l 1226 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β π β π΄) |
15 | | lnatex.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
16 | 15, 2, 3 | hlatlej2 38241 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π(joinβπΎ)π )) |
17 | 13, 14, 8, 16 | syl3anc 1371 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β π β€ (π(joinβπΎ)π )) |
18 | | simpl3r 1229 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β π = (π(joinβπΎ)π )) |
19 | 17, 18 | breqtrrd 5176 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β π β€ π) |
20 | | neeq1 3003 |
. . . . . . . 8
β’ (π = π β (π β π β π β π)) |
21 | | breq1 5151 |
. . . . . . . 8
β’ (π = π β (π β€ π β π β€ π)) |
22 | 20, 21 | anbi12d 631 |
. . . . . . 7
β’ (π = π β ((π β π β§ π β€ π) β (π β π β§ π β€ π))) |
23 | 22 | rspcev 3612 |
. . . . . 6
β’ ((π β π΄ β§ (π β π β§ π β€ π)) β βπ β π΄ (π β π β§ π β€ π)) |
24 | 8, 12, 19, 23 | syl12anc 835 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π = π) β βπ β π΄ (π β π β§ π β€ π)) |
25 | | simpl2l 1226 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π β π) β π β π΄) |
26 | | simpr 485 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π β π) β π β π) |
27 | | simpl11 1248 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π β π) β πΎ β HL) |
28 | | simpl2r 1227 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π β π) β π β π΄) |
29 | 15, 2, 3 | hlatlej1 38240 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π(joinβπΎ)π )) |
30 | 27, 25, 28, 29 | syl3anc 1371 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π β π) β π β€ (π(joinβπΎ)π )) |
31 | | simpl3r 1229 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π β π) β π = (π(joinβπΎ)π )) |
32 | 30, 31 | breqtrrd 5176 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π β π) β π β€ π) |
33 | | neeq1 3003 |
. . . . . . . 8
β’ (π = π β (π β π β π β π)) |
34 | | breq1 5151 |
. . . . . . . 8
β’ (π = π β (π β€ π β π β€ π)) |
35 | 33, 34 | anbi12d 631 |
. . . . . . 7
β’ (π = π β ((π β π β§ π β€ π) β (π β π β§ π β€ π))) |
36 | 35 | rspcev 3612 |
. . . . . 6
β’ ((π β π΄ β§ (π β π β§ π β€ π)) β βπ β π΄ (π β π β§ π β€ π)) |
37 | 25, 26, 32, 36 | syl12anc 835 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β§ π β π) β βπ β π΄ (π β π β§ π β€ π)) |
38 | 24, 37 | pm2.61dane 3029 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π = (π(joinβπΎ)π ))) β βπ β π΄ (π β π β§ π β€ π)) |
39 | 38 | 3exp 1119 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β ((π β π΄ β§ π β π΄) β ((π β π β§ π = (π(joinβπΎ)π )) β βπ β π΄ (π β π β§ π β€ π)))) |
40 | 39 | rexlimdvv 3210 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β (βπ β π΄ βπ β π΄ (π β π β§ π = (π(joinβπΎ)π )) β βπ β π΄ (π β π β§ π β€ π))) |
41 | 7, 40 | mpd 15 |
1
β’ ((πΎ β HL β§ π β π΅ β§ (πβπ) β π) β βπ β π΄ (π β π β§ π β€ π)) |