Step | Hyp | Ref
| Expression |
1 | | simp1 1136 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πΎ β HL β§ π β π»)) |
2 | | tendosp.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
3 | | tendosp.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
4 | | tendosp.e |
. . . . . 6
β’ πΈ = ((TEndoβπΎ)βπ) |
5 | 2, 3, 4 | tendocl 39941 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) |
6 | | eqid 2732 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
7 | 6, 2, 3 | ltrn1o 39298 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπΉ) β π) β (πβπΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
8 | 1, 5, 7 | syl2anc 584 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
9 | | f1ococnv1 6862 |
. . . 4
β’ ((πβπΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β (β‘(πβπΉ) β (πβπΉ)) = ( I βΎ (BaseβπΎ))) |
10 | 8, 9 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (β‘(πβπΉ) β (πβπΉ)) = ( I βΎ (BaseβπΎ))) |
11 | 10 | coeq1d 5861 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β ((β‘(πβπΉ) β (πβπΉ)) β β‘(πβπΉ)) = (( I βΎ (BaseβπΎ)) β β‘(πβπΉ))) |
12 | | simp2 1137 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β π β πΈ) |
13 | 6, 2, 4 | tendoid 39947 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ (BaseβπΎ))) = ( I βΎ
(BaseβπΎ))) |
14 | 1, 12, 13 | syl2anc 584 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβ( I βΎ (BaseβπΎ))) = ( I βΎ
(BaseβπΎ))) |
15 | 6, 2, 3 | ltrn1o 39298 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
16 | 15 | 3adant2 1131 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
17 | | f1ococnv2 6860 |
. . . . . . . . 9
β’ (πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β (πΉ β β‘πΉ) = ( I βΎ (BaseβπΎ))) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πΉ β β‘πΉ) = ( I βΎ (BaseβπΎ))) |
19 | 18 | fveq2d 6895 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβ(πΉ β β‘πΉ)) = (πβ( I βΎ (BaseβπΎ)))) |
20 | | f1ococnv2 6860 |
. . . . . . . 8
β’ ((πβπΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β ((πβπΉ) β β‘(πβπΉ)) = ( I βΎ (BaseβπΎ))) |
21 | 8, 20 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β ((πβπΉ) β β‘(πβπΉ)) = ( I βΎ (BaseβπΎ))) |
22 | 14, 19, 21 | 3eqtr4rd 2783 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β ((πβπΉ) β β‘(πβπΉ)) = (πβ(πΉ β β‘πΉ))) |
23 | | simp3 1138 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β πΉ β π) |
24 | 2, 3 | ltrncnv 39320 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |
25 | 24 | 3adant2 1131 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β β‘πΉ β π) |
26 | 2, 3, 4 | tendospdi1 40194 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΉ β π β§ β‘πΉ β π)) β (πβ(πΉ β β‘πΉ)) = ((πβπΉ) β (πββ‘πΉ))) |
27 | 1, 12, 23, 25, 26 | syl13anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβ(πΉ β β‘πΉ)) = ((πβπΉ) β (πββ‘πΉ))) |
28 | 22, 27 | eqtrd 2772 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β ((πβπΉ) β β‘(πβπΉ)) = ((πβπΉ) β (πββ‘πΉ))) |
29 | 28 | coeq2d 5862 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (β‘(πβπΉ) β ((πβπΉ) β β‘(πβπΉ))) = (β‘(πβπΉ) β ((πβπΉ) β (πββ‘πΉ)))) |
30 | | coass 6264 |
. . . 4
β’ ((β‘(πβπΉ) β (πβπΉ)) β β‘(πβπΉ)) = (β‘(πβπΉ) β ((πβπΉ) β β‘(πβπΉ))) |
31 | | coass 6264 |
. . . 4
β’ ((β‘(πβπΉ) β (πβπΉ)) β (πββ‘πΉ)) = (β‘(πβπΉ) β ((πβπΉ) β (πββ‘πΉ))) |
32 | 29, 30, 31 | 3eqtr4g 2797 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β ((β‘(πβπΉ) β (πβπΉ)) β β‘(πβπΉ)) = ((β‘(πβπΉ) β (πβπΉ)) β (πββ‘πΉ))) |
33 | 10 | coeq1d 5861 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β ((β‘(πβπΉ) β (πβπΉ)) β (πββ‘πΉ)) = (( I βΎ (BaseβπΎ)) β (πββ‘πΉ))) |
34 | 2, 3, 4 | tendocl 39941 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ β‘πΉ β π) β (πββ‘πΉ) β π) |
35 | 25, 34 | syld3an3 1409 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πββ‘πΉ) β π) |
36 | 6, 2, 3 | ltrn1o 39298 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πββ‘πΉ) β π) β (πββ‘πΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
37 | 1, 35, 36 | syl2anc 584 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πββ‘πΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
38 | | f1of 6833 |
. . . 4
β’ ((πββ‘πΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β (πββ‘πΉ):(BaseβπΎ)βΆ(BaseβπΎ)) |
39 | | fcoi2 6766 |
. . . 4
β’ ((πββ‘πΉ):(BaseβπΎ)βΆ(BaseβπΎ) β (( I βΎ (BaseβπΎ)) β (πββ‘πΉ)) = (πββ‘πΉ)) |
40 | 37, 38, 39 | 3syl 18 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (( I βΎ (BaseβπΎ)) β (πββ‘πΉ)) = (πββ‘πΉ)) |
41 | 32, 33, 40 | 3eqtrd 2776 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β ((β‘(πβπΉ) β (πβπΉ)) β β‘(πβπΉ)) = (πββ‘πΉ)) |
42 | 2, 3 | ltrncnv 39320 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπΉ) β π) β β‘(πβπΉ) β π) |
43 | 1, 5, 42 | syl2anc 584 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β β‘(πβπΉ) β π) |
44 | 6, 2, 3 | ltrn1o 39298 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ β‘(πβπΉ) β π) β β‘(πβπΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
45 | 1, 43, 44 | syl2anc 584 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β β‘(πβπΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
46 | | f1of 6833 |
. . 3
β’ (β‘(πβπΉ):(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β β‘(πβπΉ):(BaseβπΎ)βΆ(BaseβπΎ)) |
47 | | fcoi2 6766 |
. . 3
β’ (β‘(πβπΉ):(BaseβπΎ)βΆ(BaseβπΎ) β (( I βΎ (BaseβπΎ)) β β‘(πβπΉ)) = β‘(πβπΉ)) |
48 | 45, 46, 47 | 3syl 18 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (( I βΎ (BaseβπΎ)) β β‘(πβπΉ)) = β‘(πβπΉ)) |
49 | 11, 41, 48 | 3eqtr3rd 2781 |
1
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β β‘(πβπΉ) = (πββ‘πΉ)) |