Step | Hyp | Ref
| Expression |
1 | | tendoid0.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | tendoid0.h |
. . . 4
β’ π» = (LHypβπΎ) |
3 | | tendoid0.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
4 | 1, 2, 3 | cdlemftr0 39034 |
. . 3
β’ ((πΎ β HL β§ π β π») β βπ β π π β ( I βΎ π΅)) |
5 | 4 | 3ad2ant1 1134 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β βπ β π π β ( I βΎ π΅)) |
6 | | simpl1 1192 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β (πΎ β HL β§ π β π»)) |
7 | | simpl3l 1229 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β π β πΈ) |
8 | | tendoid0.e |
. . . . . . 7
β’ πΈ = ((TEndoβπΎ)βπ) |
9 | 2, 3, 8 | tendof 39229 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β π:πβΆπ) |
10 | 6, 7, 9 | syl2anc 585 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β π:πβΆπ) |
11 | | simprl 770 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β π β π) |
12 | | fvco3 6941 |
. . . . 5
β’ ((π:πβΆπ β§ π β π) β ((π β π)βπ) = (πβ(πβπ))) |
13 | 10, 11, 12 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β ((π β π)βπ) = (πβ(πβπ))) |
14 | | simpl2r 1228 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β π β π) |
15 | | simpl2l 1227 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β π β πΈ) |
16 | 2, 3, 8 | tendocl 39233 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
17 | 6, 7, 11, 16 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β (πβπ) β π) |
18 | | simpl3r 1230 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β π β π) |
19 | | simpr 486 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β (π β π β§ π β ( I βΎ π΅))) |
20 | | tendoid0.o |
. . . . . . . . . . 11
β’ π = (π β π β¦ ( I βΎ π΅)) |
21 | 1, 2, 3, 8, 20 | tendoid0 39291 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (π β π β§ π β ( I βΎ π΅))) β ((πβπ) = ( I βΎ π΅) β π = π)) |
22 | 6, 7, 19, 21 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β ((πβπ) = ( I βΎ π΅) β π = π)) |
23 | 22 | necon3bid 2989 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β ((πβπ) β ( I βΎ π΅) β π β π)) |
24 | 18, 23 | mpbird 257 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β (πβπ) β ( I βΎ π΅)) |
25 | 1, 2, 3, 8, 20 | tendoid0 39291 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ ((πβπ) β π β§ (πβπ) β ( I βΎ π΅))) β ((πβ(πβπ)) = ( I βΎ π΅) β π = π)) |
26 | 6, 15, 17, 24, 25 | syl112anc 1375 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β ((πβ(πβπ)) = ( I βΎ π΅) β π = π)) |
27 | 26 | necon3bid 2989 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β ((πβ(πβπ)) β ( I βΎ π΅) β π β π)) |
28 | 14, 27 | mpbird 257 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β (πβ(πβπ)) β ( I βΎ π΅)) |
29 | 13, 28 | eqnetrd 3012 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β ((π β π)βπ) β ( I βΎ π΅)) |
30 | 2, 8 | tendococl 39238 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π) β πΈ) |
31 | 6, 15, 7, 30 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β (π β π) β πΈ) |
32 | 1, 2, 3, 8, 20 | tendoid0 39291 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π) β πΈ β§ (π β π β§ π β ( I βΎ π΅))) β (((π β π)βπ) = ( I βΎ π΅) β (π β π) = π)) |
33 | 6, 31, 19, 32 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β (((π β π)βπ) = ( I βΎ π΅) β (π β π) = π)) |
34 | 33 | necon3bid 2989 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β (((π β π)βπ) β ( I βΎ π΅) β (π β π) β π)) |
35 | 29, 34 | mpbid 231 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β§ (π β π β§ π β ( I βΎ π΅))) β (π β π) β π) |
36 | 5, 35 | rexlimddv 3159 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β (π β π) β π) |