Step | Hyp | Ref
| Expression |
1 | | inveq.b |
. . 3
β’ π΅ = (BaseβπΆ) |
2 | | eqid 2732 |
. . 3
β’
(SectβπΆ) =
(SectβπΆ) |
3 | | inveq.c |
. . . 4
β’ (π β πΆ β Cat) |
4 | 3 | adantr 481 |
. . 3
β’ ((π β§ (πΉ(πππ)πΊ β§ πΉ(πππ)πΎ)) β πΆ β Cat) |
5 | | inveq.y |
. . . 4
β’ (π β π β π΅) |
6 | 5 | adantr 481 |
. . 3
β’ ((π β§ (πΉ(πππ)πΊ β§ πΉ(πππ)πΎ)) β π β π΅) |
7 | | inveq.x |
. . . 4
β’ (π β π β π΅) |
8 | 7 | adantr 481 |
. . 3
β’ ((π β§ (πΉ(πππ)πΊ β§ πΉ(πππ)πΎ)) β π β π΅) |
9 | | inveq.n |
. . . . . . . 8
β’ π = (InvβπΆ) |
10 | 1, 9, 3, 7, 5, 2 | isinv 17711 |
. . . . . . 7
β’ (π β (πΉ(πππ)πΊ β (πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ))) |
11 | | simpr 485 |
. . . . . . 7
β’ ((πΉ(π(SectβπΆ)π)πΊ β§ πΊ(π(SectβπΆ)π)πΉ) β πΊ(π(SectβπΆ)π)πΉ) |
12 | 10, 11 | syl6bi 252 |
. . . . . 6
β’ (π β (πΉ(πππ)πΊ β πΊ(π(SectβπΆ)π)πΉ)) |
13 | 12 | com12 32 |
. . . . 5
β’ (πΉ(πππ)πΊ β (π β πΊ(π(SectβπΆ)π)πΉ)) |
14 | 13 | adantr 481 |
. . . 4
β’ ((πΉ(πππ)πΊ β§ πΉ(πππ)πΎ) β (π β πΊ(π(SectβπΆ)π)πΉ)) |
15 | 14 | impcom 408 |
. . 3
β’ ((π β§ (πΉ(πππ)πΊ β§ πΉ(πππ)πΎ)) β πΊ(π(SectβπΆ)π)πΉ) |
16 | 1, 9, 3, 7, 5, 2 | isinv 17711 |
. . . . . 6
β’ (π β (πΉ(πππ)πΎ β (πΉ(π(SectβπΆ)π)πΎ β§ πΎ(π(SectβπΆ)π)πΉ))) |
17 | | simpl 483 |
. . . . . 6
β’ ((πΉ(π(SectβπΆ)π)πΎ β§ πΎ(π(SectβπΆ)π)πΉ) β πΉ(π(SectβπΆ)π)πΎ) |
18 | 16, 17 | syl6bi 252 |
. . . . 5
β’ (π β (πΉ(πππ)πΎ β πΉ(π(SectβπΆ)π)πΎ)) |
19 | 18 | adantld 491 |
. . . 4
β’ (π β ((πΉ(πππ)πΊ β§ πΉ(πππ)πΎ) β πΉ(π(SectβπΆ)π)πΎ)) |
20 | 19 | imp 407 |
. . 3
β’ ((π β§ (πΉ(πππ)πΊ β§ πΉ(πππ)πΎ)) β πΉ(π(SectβπΆ)π)πΎ) |
21 | 1, 2, 4, 6, 8, 15,
20 | sectcan 17706 |
. 2
β’ ((π β§ (πΉ(πππ)πΊ β§ πΉ(πππ)πΎ)) β πΊ = πΎ) |
22 | 21 | ex 413 |
1
β’ (π β ((πΉ(πππ)πΊ β§ πΉ(πππ)πΎ) β πΊ = πΎ)) |