Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . 4
β’ ((πβπ΄) = π΅ β (π΄πΊ(πβπ΄)) = (π΄πΊπ΅)) |
2 | 1 | adantl 483 |
. . 3
β’ (((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β§ (πβπ΄) = π΅) β (π΄πΊ(πβπ΄)) = (π΄πΊπ΅)) |
3 | | grpinv.1 |
. . . . . 6
β’ π = ran πΊ |
4 | | grpinv.2 |
. . . . . 6
β’ π = (GIdβπΊ) |
5 | | grpinv.3 |
. . . . . 6
β’ π = (invβπΊ) |
6 | 3, 4, 5 | grporinv 29511 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΄ β π) β (π΄πΊ(πβπ΄)) = π) |
7 | 6 | 3adant3 1133 |
. . . 4
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄πΊ(πβπ΄)) = π) |
8 | 7 | adantr 482 |
. . 3
β’ (((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β§ (πβπ΄) = π΅) β (π΄πΊ(πβπ΄)) = π) |
9 | 2, 8 | eqtr3d 2775 |
. 2
β’ (((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β§ (πβπ΄) = π΅) β (π΄πΊπ΅) = π) |
10 | | oveq2 7366 |
. . . 4
β’ ((π΄πΊπ΅) = π β ((πβπ΄)πΊ(π΄πΊπ΅)) = ((πβπ΄)πΊπ)) |
11 | 10 | adantl 483 |
. . 3
β’ (((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β§ (π΄πΊπ΅) = π) β ((πβπ΄)πΊ(π΄πΊπ΅)) = ((πβπ΄)πΊπ)) |
12 | 3, 4, 5 | grpolinv 29510 |
. . . . . . . 8
β’ ((πΊ β GrpOp β§ π΄ β π) β ((πβπ΄)πΊπ΄) = π) |
13 | 12 | oveq1d 7373 |
. . . . . . 7
β’ ((πΊ β GrpOp β§ π΄ β π) β (((πβπ΄)πΊπ΄)πΊπ΅) = (ππΊπ΅)) |
14 | 13 | 3adant3 1133 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (((πβπ΄)πΊπ΄)πΊπ΅) = (ππΊπ΅)) |
15 | 3, 5 | grpoinvcl 29508 |
. . . . . . . . . 10
β’ ((πΊ β GrpOp β§ π΄ β π) β (πβπ΄) β π) |
16 | 15 | adantrr 716 |
. . . . . . . . 9
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π)) β (πβπ΄) β π) |
17 | | simprl 770 |
. . . . . . . . 9
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π)) β π΄ β π) |
18 | | simprr 772 |
. . . . . . . . 9
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π)) β π΅ β π) |
19 | 16, 17, 18 | 3jca 1129 |
. . . . . . . 8
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π)) β ((πβπ΄) β π β§ π΄ β π β§ π΅ β π)) |
20 | 3 | grpoass 29487 |
. . . . . . . 8
β’ ((πΊ β GrpOp β§ ((πβπ΄) β π β§ π΄ β π β§ π΅ β π)) β (((πβπ΄)πΊπ΄)πΊπ΅) = ((πβπ΄)πΊ(π΄πΊπ΅))) |
21 | 19, 20 | syldan 592 |
. . . . . . 7
β’ ((πΊ β GrpOp β§ (π΄ β π β§ π΅ β π)) β (((πβπ΄)πΊπ΄)πΊπ΅) = ((πβπ΄)πΊ(π΄πΊπ΅))) |
22 | 21 | 3impb 1116 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (((πβπ΄)πΊπ΄)πΊπ΅) = ((πβπ΄)πΊ(π΄πΊπ΅))) |
23 | 14, 22 | eqtr3d 2775 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (ππΊπ΅) = ((πβπ΄)πΊ(π΄πΊπ΅))) |
24 | 3, 4 | grpolid 29500 |
. . . . . 6
β’ ((πΊ β GrpOp β§ π΅ β π) β (ππΊπ΅) = π΅) |
25 | 24 | 3adant2 1132 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (ππΊπ΅) = π΅) |
26 | 23, 25 | eqtr3d 2775 |
. . . 4
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β ((πβπ΄)πΊ(π΄πΊπ΅)) = π΅) |
27 | 26 | adantr 482 |
. . 3
β’ (((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β§ (π΄πΊπ΅) = π) β ((πβπ΄)πΊ(π΄πΊπ΅)) = π΅) |
28 | 3, 4 | grporid 29501 |
. . . . . 6
β’ ((πΊ β GrpOp β§ (πβπ΄) β π) β ((πβπ΄)πΊπ) = (πβπ΄)) |
29 | 15, 28 | syldan 592 |
. . . . 5
β’ ((πΊ β GrpOp β§ π΄ β π) β ((πβπ΄)πΊπ) = (πβπ΄)) |
30 | 29 | 3adant3 1133 |
. . . 4
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β ((πβπ΄)πΊπ) = (πβπ΄)) |
31 | 30 | adantr 482 |
. . 3
β’ (((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β§ (π΄πΊπ΅) = π) β ((πβπ΄)πΊπ) = (πβπ΄)) |
32 | 11, 27, 31 | 3eqtr3rd 2782 |
. 2
β’ (((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β§ (π΄πΊπ΅) = π) β (πβπ΄) = π΅) |
33 | 9, 32 | impbida 800 |
1
β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β ((πβπ΄) = π΅ β (π΄πΊπ΅) = π)) |