Step | Hyp | Ref
| Expression |
1 | | tendoeq2.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
2 | | tendoeq2.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
3 | | tendoeq2.e |
. . . . . . . 8
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | 1, 2, 3 | tendoid 39239 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
5 | 4 | adantrr 716 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
6 | 1, 2, 3 | tendoid 39239 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
7 | 6 | adantrl 715 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |
8 | 5, 7 | eqtr4d 2780 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (πβ( I βΎ π΅)) = (πβ( I βΎ π΅))) |
9 | | fveq2 6843 |
. . . . . 6
β’ (π = ( I βΎ π΅) β (πβπ) = (πβ( I βΎ π΅))) |
10 | | fveq2 6843 |
. . . . . 6
β’ (π = ( I βΎ π΅) β (πβπ) = (πβ( I βΎ π΅))) |
11 | 9, 10 | eqeq12d 2753 |
. . . . 5
β’ (π = ( I βΎ π΅) β ((πβπ) = (πβπ) β (πβ( I βΎ π΅)) = (πβ( I βΎ π΅)))) |
12 | 8, 11 | syl5ibrcom 247 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π = ( I βΎ π΅) β (πβπ) = (πβπ))) |
13 | 12 | ralrimivw 3148 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β βπ β π (π = ( I βΎ π΅) β (πβπ) = (πβπ))) |
14 | | r19.26 3115 |
. . . . 5
β’
(βπ β
π ((π = ( I βΎ π΅) β (πβπ) = (πβπ)) β§ (π β ( I βΎ π΅) β (πβπ) = (πβπ))) β (βπ β π (π = ( I βΎ π΅) β (πβπ) = (πβπ)) β§ βπ β π (π β ( I βΎ π΅) β (πβπ) = (πβπ)))) |
15 | | jaob 961 |
. . . . . . 7
β’ (((π = ( I βΎ π΅) β¨ π β ( I βΎ π΅)) β (πβπ) = (πβπ)) β ((π = ( I βΎ π΅) β (πβπ) = (πβπ)) β§ (π β ( I βΎ π΅) β (πβπ) = (πβπ)))) |
16 | | exmidne 2954 |
. . . . . . . 8
β’ (π = ( I βΎ π΅) β¨ π β ( I βΎ π΅)) |
17 | | pm5.5 362 |
. . . . . . . 8
β’ ((π = ( I βΎ π΅) β¨ π β ( I βΎ π΅)) β (((π = ( I βΎ π΅) β¨ π β ( I βΎ π΅)) β (πβπ) = (πβπ)) β (πβπ) = (πβπ))) |
18 | 16, 17 | ax-mp 5 |
. . . . . . 7
β’ (((π = ( I βΎ π΅) β¨ π β ( I βΎ π΅)) β (πβπ) = (πβπ)) β (πβπ) = (πβπ)) |
19 | 15, 18 | bitr3i 277 |
. . . . . 6
β’ (((π = ( I βΎ π΅) β (πβπ) = (πβπ)) β§ (π β ( I βΎ π΅) β (πβπ) = (πβπ))) β (πβπ) = (πβπ)) |
20 | 19 | ralbii 3097 |
. . . . 5
β’
(βπ β
π ((π = ( I βΎ π΅) β (πβπ) = (πβπ)) β§ (π β ( I βΎ π΅) β (πβπ) = (πβπ))) β βπ β π (πβπ) = (πβπ)) |
21 | 14, 20 | bitr3i 277 |
. . . 4
β’
((βπ β
π (π = ( I βΎ π΅) β (πβπ) = (πβπ)) β§ βπ β π (π β ( I βΎ π΅) β (πβπ) = (πβπ))) β βπ β π (πβπ) = (πβπ)) |
22 | | tendoeq2.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
23 | 2, 22, 3 | tendoeq1 39230 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ βπ β π (πβπ) = (πβπ)) β π = π) |
24 | 23 | 3expia 1122 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (βπ β π (πβπ) = (πβπ) β π = π)) |
25 | 21, 24 | biimtrid 241 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β ((βπ β π (π = ( I βΎ π΅) β (πβπ) = (πβπ)) β§ βπ β π (π β ( I βΎ π΅) β (πβπ) = (πβπ))) β π = π)) |
26 | 13, 25 | mpand 694 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (βπ β π (π β ( I βΎ π΅) β (πβπ) = (πβπ)) β π = π)) |
27 | 26 | 3impia 1118 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ βπ β π (π β ( I βΎ π΅) β (πβπ) = (πβπ))) β π = π) |