Step | Hyp | Ref
| Expression |
1 | | df-vs 29852 |
. . . . 5
β’
βπ£ = ( /π β
+π£ ) |
2 | 1 | fveq1i 6893 |
. . . 4
β’ (
βπ£ βπ) = (( /π β
+π£ )βπ) |
3 | | fo1st 7995 |
. . . . . . . 8
β’
1st :VβontoβV |
4 | | fof 6806 |
. . . . . . . 8
β’
(1st :VβontoβV β 1st
:VβΆV) |
5 | 3, 4 | ax-mp 5 |
. . . . . . 7
β’
1st :VβΆV |
6 | | fco 6742 |
. . . . . . 7
β’
((1st :VβΆV β§ 1st :VβΆV) β
(1st β 1st ):VβΆV) |
7 | 5, 5, 6 | mp2an 691 |
. . . . . 6
β’
(1st β 1st ):VβΆV |
8 | | df-va 29848 |
. . . . . . 7
β’
+π£ = (1st β 1st
) |
9 | 8 | feq1i 6709 |
. . . . . 6
β’ (
+π£ :VβΆV β (1st β 1st
):VβΆV) |
10 | 7, 9 | mpbir 230 |
. . . . 5
β’
+π£ :VβΆV |
11 | | fvco3 6991 |
. . . . 5
β’ ((
+π£ :VβΆV β§ π β V) β (( /π
β +π£ )βπ) = ( /π β(
+π£ βπ))) |
12 | 10, 11 | mpan 689 |
. . . 4
β’ (π β V β ((
/π β +π£ )βπ) = ( /π β(
+π£ βπ))) |
13 | 2, 12 | eqtrid 2785 |
. . 3
β’ (π β V β (
βπ£ βπ) = ( /π β(
+π£ βπ))) |
14 | | 0ngrp 29764 |
. . . . . 6
β’ Β¬
β
β GrpOp |
15 | | vex 3479 |
. . . . . . . . . 10
β’ π β V |
16 | 15 | rnex 7903 |
. . . . . . . . 9
β’ ran π β V |
17 | 16, 16 | mpoex 8066 |
. . . . . . . 8
β’ (π₯ β ran π, π¦ β ran π β¦ (π₯π((invβπ)βπ¦))) β V |
18 | | df-gdiv 29749 |
. . . . . . . 8
β’
/π = (π
β GrpOp β¦ (π₯
β ran π, π¦ β ran π β¦ (π₯π((invβπ)βπ¦)))) |
19 | 17, 18 | dmmpti 6695 |
. . . . . . 7
β’ dom
/π = GrpOp |
20 | 19 | eleq2i 2826 |
. . . . . 6
β’ (β
β dom /π β β
β GrpOp) |
21 | 14, 20 | mtbir 323 |
. . . . 5
β’ Β¬
β
β dom /π |
22 | | ndmfv 6927 |
. . . . 5
β’ (Β¬
β
β dom /π β ( /π
ββ
) = β
) |
23 | 21, 22 | mp1i 13 |
. . . 4
β’ (Β¬
π β V β (
/π ββ
) = β
) |
24 | | fvprc 6884 |
. . . . 5
β’ (Β¬
π β V β (
+π£ βπ) = β
) |
25 | 24 | fveq2d 6896 |
. . . 4
β’ (Β¬
π β V β (
/π β( +π£ βπ)) = ( /π
ββ
)) |
26 | | fvprc 6884 |
. . . 4
β’ (Β¬
π β V β (
βπ£ βπ) = β
) |
27 | 23, 25, 26 | 3eqtr4rd 2784 |
. . 3
β’ (Β¬
π β V β (
βπ£ βπ) = ( /π β(
+π£ βπ))) |
28 | 13, 27 | pm2.61i 182 |
. 2
β’ (
βπ£ βπ) = ( /π β(
+π£ βπ)) |
29 | | vsfval.3 |
. 2
β’ π = ( βπ£
βπ) |
30 | | vsfval.2 |
. . 3
β’ πΊ = ( +π£
βπ) |
31 | 30 | fveq2i 6895 |
. 2
β’ (
/π βπΊ) = ( /π β(
+π£ βπ)) |
32 | 28, 29, 31 | 3eqtr4i 2771 |
1
β’ π = ( /π
βπΊ) |