Step | Hyp | Ref
| Expression |
1 | | oveq2 7358 |
. . . . . 6
β’ ((πΆπΊπ΄) = (πΆπΊπ΅) β (((invβπΊ)βπΆ)πΊ(πΆπΊπ΄)) = (((invβπΊ)βπΆ)πΊ(πΆπΊπ΅))) |
2 | 1 | adantl 483 |
. . . . 5
β’ ((((πΊ β GrpOp β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β§ (πΆπΊπ΄) = (πΆπΊπ΅)) β (((invβπΊ)βπΆ)πΊ(πΆπΊπ΄)) = (((invβπΊ)βπΆ)πΊ(πΆπΊπ΅))) |
3 | | grplcan.1 |
. . . . . . . . . . 11
β’ π = ran πΊ |
4 | | eqid 2738 |
. . . . . . . . . . 11
β’
(GIdβπΊ) =
(GIdβπΊ) |
5 | | eqid 2738 |
. . . . . . . . . . 11
β’
(invβπΊ) =
(invβπΊ) |
6 | 3, 4, 5 | grpolinv 29254 |
. . . . . . . . . 10
β’ ((πΊ β GrpOp β§ πΆ β π) β (((invβπΊ)βπΆ)πΊπΆ) = (GIdβπΊ)) |
7 | 6 | adantlr 714 |
. . . . . . . . 9
β’ (((πΊ β GrpOp β§ π΄ β π) β§ πΆ β π) β (((invβπΊ)βπΆ)πΊπΆ) = (GIdβπΊ)) |
8 | 7 | oveq1d 7365 |
. . . . . . . 8
β’ (((πΊ β GrpOp β§ π΄ β π) β§ πΆ β π) β ((((invβπΊ)βπΆ)πΊπΆ)πΊπ΄) = ((GIdβπΊ)πΊπ΄)) |
9 | 3, 5 | grpoinvcl 29252 |
. . . . . . . . . . . 12
β’ ((πΊ β GrpOp β§ πΆ β π) β ((invβπΊ)βπΆ) β π) |
10 | 9 | adantrl 715 |
. . . . . . . . . . 11
β’ ((πΊ β GrpOp β§ (π΄ β π β§ πΆ β π)) β ((invβπΊ)βπΆ) β π) |
11 | | simprr 772 |
. . . . . . . . . . 11
β’ ((πΊ β GrpOp β§ (π΄ β π β§ πΆ β π)) β πΆ β π) |
12 | | simprl 770 |
. . . . . . . . . . 11
β’ ((πΊ β GrpOp β§ (π΄ β π β§ πΆ β π)) β π΄ β π) |
13 | 10, 11, 12 | 3jca 1129 |
. . . . . . . . . 10
β’ ((πΊ β GrpOp β§ (π΄ β π β§ πΆ β π)) β (((invβπΊ)βπΆ) β π β§ πΆ β π β§ π΄ β π)) |
14 | 3 | grpoass 29231 |
. . . . . . . . . 10
β’ ((πΊ β GrpOp β§
(((invβπΊ)βπΆ) β π β§ πΆ β π β§ π΄ β π)) β ((((invβπΊ)βπΆ)πΊπΆ)πΊπ΄) = (((invβπΊ)βπΆ)πΊ(πΆπΊπ΄))) |
15 | 13, 14 | syldan 592 |
. . . . . . . . 9
β’ ((πΊ β GrpOp β§ (π΄ β π β§ πΆ β π)) β ((((invβπΊ)βπΆ)πΊπΆ)πΊπ΄) = (((invβπΊ)βπΆ)πΊ(πΆπΊπ΄))) |
16 | 15 | anassrs 469 |
. . . . . . . 8
β’ (((πΊ β GrpOp β§ π΄ β π) β§ πΆ β π) β ((((invβπΊ)βπΆ)πΊπΆ)πΊπ΄) = (((invβπΊ)βπΆ)πΊ(πΆπΊπ΄))) |
17 | 3, 4 | grpolid 29244 |
. . . . . . . . 9
β’ ((πΊ β GrpOp β§ π΄ β π) β ((GIdβπΊ)πΊπ΄) = π΄) |
18 | 17 | adantr 482 |
. . . . . . . 8
β’ (((πΊ β GrpOp β§ π΄ β π) β§ πΆ β π) β ((GIdβπΊ)πΊπ΄) = π΄) |
19 | 8, 16, 18 | 3eqtr3d 2786 |
. . . . . . 7
β’ (((πΊ β GrpOp β§ π΄ β π) β§ πΆ β π) β (((invβπΊ)βπΆ)πΊ(πΆπΊπ΄)) = π΄) |
20 | 19 | adantrl 715 |
. . . . . 6
β’ (((πΊ β GrpOp β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β (((invβπΊ)βπΆ)πΊ(πΆπΊπ΄)) = π΄) |
21 | 20 | adantr 482 |
. . . . 5
β’ ((((πΊ β GrpOp β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β§ (πΆπΊπ΄) = (πΆπΊπ΅)) β (((invβπΊ)βπΆ)πΊ(πΆπΊπ΄)) = π΄) |
22 | 6 | adantrl 715 |
. . . . . . . . 9
β’ ((πΊ β GrpOp β§ (π΅ β π β§ πΆ β π)) β (((invβπΊ)βπΆ)πΊπΆ) = (GIdβπΊ)) |
23 | 22 | oveq1d 7365 |
. . . . . . . 8
β’ ((πΊ β GrpOp β§ (π΅ β π β§ πΆ β π)) β ((((invβπΊ)βπΆ)πΊπΆ)πΊπ΅) = ((GIdβπΊ)πΊπ΅)) |
24 | 9 | adantrl 715 |
. . . . . . . . . 10
β’ ((πΊ β GrpOp β§ (π΅ β π β§ πΆ β π)) β ((invβπΊ)βπΆ) β π) |
25 | | simprr 772 |
. . . . . . . . . 10
β’ ((πΊ β GrpOp β§ (π΅ β π β§ πΆ β π)) β πΆ β π) |
26 | | simprl 770 |
. . . . . . . . . 10
β’ ((πΊ β GrpOp β§ (π΅ β π β§ πΆ β π)) β π΅ β π) |
27 | 24, 25, 26 | 3jca 1129 |
. . . . . . . . 9
β’ ((πΊ β GrpOp β§ (π΅ β π β§ πΆ β π)) β (((invβπΊ)βπΆ) β π β§ πΆ β π β§ π΅ β π)) |
28 | 3 | grpoass 29231 |
. . . . . . . . 9
β’ ((πΊ β GrpOp β§
(((invβπΊ)βπΆ) β π β§ πΆ β π β§ π΅ β π)) β ((((invβπΊ)βπΆ)πΊπΆ)πΊπ΅) = (((invβπΊ)βπΆ)πΊ(πΆπΊπ΅))) |
29 | 27, 28 | syldan 592 |
. . . . . . . 8
β’ ((πΊ β GrpOp β§ (π΅ β π β§ πΆ β π)) β ((((invβπΊ)βπΆ)πΊπΆ)πΊπ΅) = (((invβπΊ)βπΆ)πΊ(πΆπΊπ΅))) |
30 | 3, 4 | grpolid 29244 |
. . . . . . . . 9
β’ ((πΊ β GrpOp β§ π΅ β π) β ((GIdβπΊ)πΊπ΅) = π΅) |
31 | 30 | adantrr 716 |
. . . . . . . 8
β’ ((πΊ β GrpOp β§ (π΅ β π β§ πΆ β π)) β ((GIdβπΊ)πΊπ΅) = π΅) |
32 | 23, 29, 31 | 3eqtr3d 2786 |
. . . . . . 7
β’ ((πΊ β GrpOp β§ (π΅ β π β§ πΆ β π)) β (((invβπΊ)βπΆ)πΊ(πΆπΊπ΅)) = π΅) |
33 | 32 | adantlr 714 |
. . . . . 6
β’ (((πΊ β GrpOp β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β (((invβπΊ)βπΆ)πΊ(πΆπΊπ΅)) = π΅) |
34 | 33 | adantr 482 |
. . . . 5
β’ ((((πΊ β GrpOp β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β§ (πΆπΊπ΄) = (πΆπΊπ΅)) β (((invβπΊ)βπΆ)πΊ(πΆπΊπ΅)) = π΅) |
35 | 2, 21, 34 | 3eqtr3d 2786 |
. . . 4
β’ ((((πΊ β GrpOp β§ π΄ β π) β§ (π΅ β π β§ πΆ β π)) β§ (πΆπΊπ΄) = (πΆπΊπ΅)) β π΄ = π΅) |
36 | 35 | exp53 449 |
. . 3
β’ (πΊ β GrpOp β (π΄ β π β (π΅ β π β (πΆ β π β ((πΆπΊπ΄) = (πΆπΊπ΅) β π΄ = π΅))))) |
37 | 36 | 3imp2 1350 |
. 2
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆπΊπ΄) = (πΆπΊπ΅) β π΄ = π΅)) |
38 | | oveq2 7358 |
. 2
β’ (π΄ = π΅ β (πΆπΊπ΄) = (πΆπΊπ΅)) |
39 | 37, 38 | impbid1 224 |
1
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆπΊπ΄) = (πΆπΊπ΅) β π΄ = π΅)) |