Step | Hyp | Ref
| Expression |
1 | | dia11.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
2 | | dia11.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | dia11.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | | eqid 2733 |
. . . . 5
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
5 | | eqid 2733 |
. . . . 5
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
6 | | dia11.i |
. . . . 5
β’ πΌ = ((DIsoAβπΎ)βπ) |
7 | 1, 2, 3, 4, 5, 6 | diaval 39545 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π}) |
8 | 7 | 3adant3 1133 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π}) |
9 | 1, 2, 3, 4, 5, 6 | diaval 39545 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π}) |
10 | 9 | 3adant2 1132 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π}) |
11 | 8, 10 | sseq12d 3981 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β ((πΌβπ) β (πΌβπ) β {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π} β {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π})) |
12 | | ss2rab 4032 |
. . 3
β’ ({π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π} β {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π} β βπ β ((LTrnβπΎ)βπ)((((trLβπΎ)βπ)βπ) β€ π β (((trLβπΎ)βπ)βπ) β€ π)) |
13 | | eqid 2733 |
. . . 4
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
14 | 1, 2, 13, 3, 4, 5 | trlord 39082 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β (π β€ π β βπ β ((LTrnβπΎ)βπ)((((trLβπΎ)βπ)βπ) β€ π β (((trLβπΎ)βπ)βπ) β€ π))) |
15 | 12, 14 | bitr4id 290 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β ({π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π} β {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ) β€ π} β π β€ π)) |
16 | 11, 15 | bitrd 279 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) |