Step | Hyp | Ref
| Expression |
1 | | grpinvfval.3 |
. 2
β’ π = (invβπΊ) |
2 | | grpinvfval.1 |
. . . . 5
β’ π = ran πΊ |
3 | | rnexg 7832 |
. . . . 5
β’ (πΊ β GrpOp β ran πΊ β V) |
4 | 2, 3 | eqeltrid 2843 |
. . . 4
β’ (πΊ β GrpOp β π β V) |
5 | | mptexg 7166 |
. . . 4
β’ (π β V β (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = π)) β V) |
6 | 4, 5 | syl 17 |
. . 3
β’ (πΊ β GrpOp β (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = π)) β V) |
7 | | rneq 5888 |
. . . . . 6
β’ (π = πΊ β ran π = ran πΊ) |
8 | 7, 2 | eqtr4di 2796 |
. . . . 5
β’ (π = πΊ β ran π = π) |
9 | | oveq 7356 |
. . . . . . 7
β’ (π = πΊ β (π¦ππ₯) = (π¦πΊπ₯)) |
10 | | fveq2 6838 |
. . . . . . . 8
β’ (π = πΊ β (GIdβπ) = (GIdβπΊ)) |
11 | | grpinvfval.2 |
. . . . . . . 8
β’ π = (GIdβπΊ) |
12 | 10, 11 | eqtr4di 2796 |
. . . . . . 7
β’ (π = πΊ β (GIdβπ) = π) |
13 | 9, 12 | eqeq12d 2754 |
. . . . . 6
β’ (π = πΊ β ((π¦ππ₯) = (GIdβπ) β (π¦πΊπ₯) = π)) |
14 | 8, 13 | riotaeqbidv 7309 |
. . . . 5
β’ (π = πΊ β (β©π¦ β ran π(π¦ππ₯) = (GIdβπ)) = (β©π¦ β π (π¦πΊπ₯) = π)) |
15 | 8, 14 | mpteq12dv 5195 |
. . . 4
β’ (π = πΊ β (π₯ β ran π β¦ (β©π¦ β ran π(π¦ππ₯) = (GIdβπ))) = (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = π))) |
16 | | df-ginv 29223 |
. . . 4
β’ inv =
(π β GrpOp β¦
(π₯ β ran π β¦ (β©π¦ β ran π(π¦ππ₯) = (GIdβπ)))) |
17 | 15, 16 | fvmptg 6942 |
. . 3
β’ ((πΊ β GrpOp β§ (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = π)) β V) β (invβπΊ) = (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = π))) |
18 | 6, 17 | mpdan 686 |
. 2
β’ (πΊ β GrpOp β
(invβπΊ) = (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = π))) |
19 | 1, 18 | eqtrid 2790 |
1
β’ (πΊ β GrpOp β π = (π₯ β π β¦ (β©π¦ β π (π¦πΊπ₯) = π))) |