Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. 2
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | tendopltp.l |
. 2
β’ β€ =
(leβπΎ) |
3 | | simp1l 1197 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β πΎ β HL) |
4 | 3 | hllatd 38320 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β πΎ β Lat) |
5 | | simp1 1136 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (πΎ β HL β§ π β π»)) |
6 | | tendopl.h |
. . . 4
β’ π» = (LHypβπΎ) |
7 | | tendopl.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
8 | | tendopl.e |
. . . 4
β’ πΈ = ((TEndoβπΎ)βπ) |
9 | | tendopl.p |
. . . 4
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) |
10 | 6, 7, 8, 9 | tendoplcl2 39735 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β ((πππ)βπΉ) β π) |
11 | | tendopltp.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
12 | 1, 6, 7, 11 | trlcl 39121 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((πππ)βπΉ) β π) β (π
β((πππ)βπΉ)) β (BaseβπΎ)) |
13 | 5, 10, 12 | syl2anc 584 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
β((πππ)βπΉ)) β (BaseβπΎ)) |
14 | 6, 7, 8 | tendocl 39724 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) |
15 | 14 | 3adant2r 1179 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (πβπΉ) β π) |
16 | 1, 6, 7, 11 | trlcl 39121 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πβπΉ) β π) β (π
β(πβπΉ)) β (BaseβπΎ)) |
17 | 5, 15, 16 | syl2anc 584 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
β(πβπΉ)) β (BaseβπΎ)) |
18 | 6, 7, 8 | tendocl 39724 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) |
19 | 18 | 3adant2l 1178 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (πβπΉ) β π) |
20 | 1, 6, 7, 11 | trlcl 39121 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πβπΉ) β π) β (π
β(πβπΉ)) β (BaseβπΎ)) |
21 | 5, 19, 20 | syl2anc 584 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
β(πβπΉ)) β (BaseβπΎ)) |
22 | | eqid 2732 |
. . . 4
β’
(joinβπΎ) =
(joinβπΎ) |
23 | 1, 22 | latjcl 18394 |
. . 3
β’ ((πΎ β Lat β§ (π
β(πβπΉ)) β (BaseβπΎ) β§ (π
β(πβπΉ)) β (BaseβπΎ)) β ((π
β(πβπΉ))(joinβπΎ)(π
β(πβπΉ))) β (BaseβπΎ)) |
24 | 4, 17, 21, 23 | syl3anc 1371 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β ((π
β(πβπΉ))(joinβπΎ)(π
β(πβπΉ))) β (BaseβπΎ)) |
25 | | simp3 1138 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β πΉ β π) |
26 | 1, 6, 7, 11 | trlcl 39121 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β (BaseβπΎ)) |
27 | 5, 25, 26 | syl2anc 584 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
βπΉ) β (BaseβπΎ)) |
28 | | simp2l 1199 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β π β πΈ) |
29 | | simp2r 1200 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β π β πΈ) |
30 | 9, 7 | tendopl2 39734 |
. . . . 5
β’ ((π β πΈ β§ π β πΈ β§ πΉ β π) β ((πππ)βπΉ) = ((πβπΉ) β (πβπΉ))) |
31 | 28, 29, 25, 30 | syl3anc 1371 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β ((πππ)βπΉ) = ((πβπΉ) β (πβπΉ))) |
32 | 31 | fveq2d 6895 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
β((πππ)βπΉ)) = (π
β((πβπΉ) β (πβπΉ)))) |
33 | 2, 22, 6, 7, 11 | trlco 39684 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πβπΉ) β π β§ (πβπΉ) β π) β (π
β((πβπΉ) β (πβπΉ))) β€ ((π
β(πβπΉ))(joinβπΎ)(π
β(πβπΉ)))) |
34 | 5, 15, 19, 33 | syl3anc 1371 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
β((πβπΉ) β (πβπΉ))) β€ ((π
β(πβπΉ))(joinβπΎ)(π
β(πβπΉ)))) |
35 | 32, 34 | eqbrtrd 5170 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
β((πππ)βπΉ)) β€ ((π
β(πβπΉ))(joinβπΎ)(π
β(πβπΉ)))) |
36 | 2, 6, 7, 11, 8 | tendotp 39718 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (π
β(πβπΉ)) β€ (π
βπΉ)) |
37 | 36 | 3adant2r 1179 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
β(πβπΉ)) β€ (π
βπΉ)) |
38 | 2, 6, 7, 11, 8 | tendotp 39718 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (π
β(πβπΉ)) β€ (π
βπΉ)) |
39 | 38 | 3adant2l 1178 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
β(πβπΉ)) β€ (π
βπΉ)) |
40 | 1, 2, 22 | latjle12 18405 |
. . . 4
β’ ((πΎ β Lat β§ ((π
β(πβπΉ)) β (BaseβπΎ) β§ (π
β(πβπΉ)) β (BaseβπΎ) β§ (π
βπΉ) β (BaseβπΎ))) β (((π
β(πβπΉ)) β€ (π
βπΉ) β§ (π
β(πβπΉ)) β€ (π
βπΉ)) β ((π
β(πβπΉ))(joinβπΎ)(π
β(πβπΉ))) β€ (π
βπΉ))) |
41 | 4, 17, 21, 27, 40 | syl13anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (((π
β(πβπΉ)) β€ (π
βπΉ) β§ (π
β(πβπΉ)) β€ (π
βπΉ)) β ((π
β(πβπΉ))(joinβπΎ)(π
β(πβπΉ))) β€ (π
βπΉ))) |
42 | 37, 39, 41 | mpbi2and 710 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β ((π
β(πβπΉ))(joinβπΎ)(π
β(πβπΉ))) β€ (π
βπΉ)) |
43 | 1, 2, 4, 13, 24, 27, 35, 42 | lattrd 18401 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π
β((πππ)βπΉ)) β€ (π
βπΉ)) |