Step | Hyp | Ref
| Expression |
1 | | tendospcan.h |
. . . . . . . . . . . . . . . . . 18
β’ π» = (LHypβπΎ) |
2 | | tendospcan.t |
. . . . . . . . . . . . . . . . . 18
β’ π = ((LTrnβπΎ)βπ) |
3 | | tendospcan.e |
. . . . . . . . . . . . . . . . . 18
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | 1, 2, 3 | tendocnv 39534 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΊ β π) β β‘(πβπΊ) = (πββ‘πΊ)) |
5 | 4 | 3adant3l 1181 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β β‘(πβπΊ) = (πββ‘πΊ)) |
6 | 5 | coeq2d 5822 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β ((πβπΉ) β β‘(πβπΊ)) = ((πβπΉ) β (πββ‘πΊ))) |
7 | | simp1 1137 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β (πΎ β HL β§ π β π»)) |
8 | | simp2 1138 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β π β πΈ) |
9 | | simp3l 1202 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β πΉ β π) |
10 | | simp3r 1203 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β πΊ β π) |
11 | 1, 2 | ltrncnv 38659 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β β‘πΊ β π) |
12 | 7, 10, 11 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β β‘πΊ β π) |
13 | 1, 2, 3 | tendospdi1 39533 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΉ β π β§ β‘πΊ β π)) β (πβ(πΉ β β‘πΊ)) = ((πβπΉ) β (πββ‘πΊ))) |
14 | 7, 8, 9, 12, 13 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β (πβ(πΉ β β‘πΊ)) = ((πβπΉ) β (πββ‘πΊ))) |
15 | 6, 14 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β ((πβπΉ) β β‘(πβπΊ)) = (πβ(πΉ β β‘πΊ))) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β ((πβπΉ) β β‘(πβπΊ)) = (πβ(πΉ β β‘πΊ))) |
17 | 16 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β (((πβπΉ) β β‘(πβπΊ)) = ( I βΎ π΅) β (πβ(πΉ β β‘πΊ)) = ( I βΎ π΅))) |
18 | | simpl1 1192 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β (πΎ β HL β§ π β π»)) |
19 | | simpl2 1193 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β π β πΈ) |
20 | | simpl3l 1229 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β πΉ β π) |
21 | 1, 2, 3 | tendocl 39280 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) |
22 | 18, 19, 20, 21 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β (πβπΉ) β π) |
23 | | simpl3r 1230 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β πΊ β π) |
24 | 1, 2, 3 | tendocl 39280 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΊ β π) β (πβπΊ) β π) |
25 | 18, 19, 23, 24 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β (πβπΊ) β π) |
26 | | tendospcan.b |
. . . . . . . . . . . . . 14
β’ π΅ = (BaseβπΎ) |
27 | 26, 1, 2 | ltrncoidN 38641 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ (πβπΉ) β π β§ (πβπΊ) β π) β (((πβπΉ) β β‘(πβπΊ)) = ( I βΎ π΅) β (πβπΉ) = (πβπΊ))) |
28 | 18, 22, 25, 27 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β (((πβπΉ) β β‘(πβπΊ)) = ( I βΎ π΅) β (πβπΉ) = (πβπΊ))) |
29 | 18, 23, 11 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β β‘πΊ β π) |
30 | 1, 2 | ltrnco 39232 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ β‘πΊ β π) β (πΉ β β‘πΊ) β π) |
31 | 18, 20, 29, 30 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β (πΉ β β‘πΊ) β π) |
32 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β (πΉ β β‘πΊ) β ( I βΎ π΅)) |
33 | | tendospcan.o |
. . . . . . . . . . . . . 14
β’ π = (π β π β¦ ( I βΎ π΅)) |
34 | 26, 1, 2, 3, 33 | tendoid0 39338 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ ((πΉ β β‘πΊ) β π β§ (πΉ β β‘πΊ) β ( I βΎ π΅))) β ((πβ(πΉ β β‘πΊ)) = ( I βΎ π΅) β π = π)) |
35 | 18, 19, 31, 32, 34 | syl112anc 1375 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β ((πβ(πΉ β β‘πΊ)) = ( I βΎ π΅) β π = π)) |
36 | 17, 28, 35 | 3bitr3d 309 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β ((πβπΉ) = (πβπΊ) β π = π)) |
37 | 36 | biimpd 228 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πΉ β β‘πΊ) β ( I βΎ π΅)) β ((πβπΉ) = (πβπΊ) β π = π)) |
38 | 37 | impancom 453 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πβπΉ) = (πβπΊ)) β ((πΉ β β‘πΊ) β ( I βΎ π΅) β π = π)) |
39 | 38 | necon1d 2962 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πβπΉ) = (πβπΊ)) β (π β π β (πΉ β β‘πΊ) = ( I βΎ π΅))) |
40 | | simpl1 1192 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πβπΉ) = (πβπΊ)) β (πΎ β HL β§ π β π»)) |
41 | | simpl3l 1229 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πβπΉ) = (πβπΊ)) β πΉ β π) |
42 | | simpl3r 1230 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πβπΉ) = (πβπΊ)) β πΊ β π) |
43 | 26, 1, 2 | ltrncoidN 38641 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β ((πΉ β β‘πΊ) = ( I βΎ π΅) β πΉ = πΊ)) |
44 | 40, 41, 42, 43 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πβπΉ) = (πβπΊ)) β ((πΉ β β‘πΊ) = ( I βΎ π΅) β πΉ = πΊ)) |
45 | 39, 44 | sylibd 238 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΊ β π)) β§ (πβπΉ) = (πβπΊ)) β (π β π β πΉ = πΊ)) |
46 | 45 | 3exp1 1353 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β (π β πΈ β ((πΉ β π β§ πΊ β π) β ((πβπΉ) = (πβπΊ) β (π β π β πΉ = πΊ))))) |
47 | 46 | com24 95 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β ((πβπΉ) = (πβπΊ) β ((πΉ β π β§ πΊ β π) β (π β πΈ β (π β π β πΉ = πΊ))))) |
48 | 47 | imp5a 442 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ((πβπΉ) = (πβπΊ) β ((πΉ β π β§ πΊ β π) β ((π β πΈ β§ π β π) β πΉ = πΊ)))) |
49 | 48 | com24 95 |
. . 3
β’ ((πΎ β HL β§ π β π») β ((π β πΈ β§ π β π) β ((πΉ β π β§ πΊ β π) β ((πβπΉ) = (πβπΊ) β πΉ = πΊ)))) |
50 | 49 | 3imp 1112 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (πΉ β π β§ πΊ β π)) β ((πβπΉ) = (πβπΊ) β πΉ = πΊ)) |
51 | | fveq2 6846 |
. 2
β’ (πΉ = πΊ β (πβπΉ) = (πβπΊ)) |
52 | 50, 51 | impbid1 224 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (πΉ β π β§ πΊ β π)) β ((πβπΉ) = (πβπΊ) β πΉ = πΊ)) |