Step | Hyp | Ref
| Expression |
1 | | psgninv.s |
. . . . 5
β’ π = (SymGrpβπ·) |
2 | | psgninv.n |
. . . . 5
β’ π = (pmSgnβπ·) |
3 | | eqid 2733 |
. . . . 5
β’
((mulGrpββfld) βΎs {1, -1}) =
((mulGrpββfld) βΎs {1,
-1}) |
4 | 1, 2, 3 | psgnghm2 21008 |
. . . 4
β’ (π· β Fin β π β (π GrpHom
((mulGrpββfld) βΎs {1,
-1}))) |
5 | | psgninv.p |
. . . . 5
β’ π = (Baseβπ) |
6 | | eqid 2733 |
. . . . 5
β’
(invgβπ) = (invgβπ) |
7 | | eqid 2733 |
. . . . 5
β’
(invgβ((mulGrpββfld)
βΎs {1, -1})) =
(invgβ((mulGrpββfld)
βΎs {1, -1})) |
8 | 5, 6, 7 | ghminv 19023 |
. . . 4
β’ ((π β (π GrpHom
((mulGrpββfld) βΎs {1, -1})) β§ πΉ β π) β (πβ((invgβπ)βπΉ)) =
((invgβ((mulGrpββfld)
βΎs {1, -1}))β(πβπΉ))) |
9 | 4, 8 | sylan 581 |
. . 3
β’ ((π· β Fin β§ πΉ β π) β (πβ((invgβπ)βπΉ)) =
((invgβ((mulGrpββfld)
βΎs {1, -1}))β(πβπΉ))) |
10 | 1, 5, 6 | symginv 19192 |
. . . . 5
β’ (πΉ β π β ((invgβπ)βπΉ) = β‘πΉ) |
11 | 10 | adantl 483 |
. . . 4
β’ ((π· β Fin β§ πΉ β π) β ((invgβπ)βπΉ) = β‘πΉ) |
12 | 11 | fveq2d 6850 |
. . 3
β’ ((π· β Fin β§ πΉ β π) β (πβ((invgβπ)βπΉ)) = (πββ‘πΉ)) |
13 | | eqid 2733 |
. . . . . 6
β’
((mulGrpββfld) βΎs (β
β {0})) = ((mulGrpββfld) βΎs
(β β {0})) |
14 | 13 | cnmsgnsubg 21004 |
. . . . 5
β’ {1, -1}
β (SubGrpβ((mulGrpββfld) βΎs
(β β {0}))) |
15 | 3 | cnmsgnbas 21005 |
. . . . . . . 8
β’ {1, -1} =
(Baseβ((mulGrpββfld) βΎs {1,
-1})) |
16 | 5, 15 | ghmf 19020 |
. . . . . . 7
β’ (π β (π GrpHom
((mulGrpββfld) βΎs {1, -1})) β
π:πβΆ{1, -1}) |
17 | 4, 16 | syl 17 |
. . . . . 6
β’ (π· β Fin β π:πβΆ{1, -1}) |
18 | 17 | ffvelcdmda 7039 |
. . . . 5
β’ ((π· β Fin β§ πΉ β π) β (πβπΉ) β {1, -1}) |
19 | | cnex 11140 |
. . . . . . . . 9
β’ β
β V |
20 | 19 | difexi 5289 |
. . . . . . . 8
β’ (β
β {0}) β V |
21 | | ax-1cn 11117 |
. . . . . . . . . 10
β’ 1 β
β |
22 | | ax-1ne0 11128 |
. . . . . . . . . 10
β’ 1 β
0 |
23 | | eldifsn 4751 |
. . . . . . . . . 10
β’ (1 β
(β β {0}) β (1 β β β§ 1 β
0)) |
24 | 21, 22, 23 | mpbir2an 710 |
. . . . . . . . 9
β’ 1 β
(β β {0}) |
25 | | neg1cn 12275 |
. . . . . . . . . 10
β’ -1 β
β |
26 | | neg1ne0 12277 |
. . . . . . . . . 10
β’ -1 β
0 |
27 | | eldifsn 4751 |
. . . . . . . . . 10
β’ (-1
β (β β {0}) β (-1 β β β§ -1 β
0)) |
28 | 25, 26, 27 | mpbir2an 710 |
. . . . . . . . 9
β’ -1 β
(β β {0}) |
29 | | prssi 4785 |
. . . . . . . . 9
β’ ((1
β (β β {0}) β§ -1 β (β β {0})) β {1,
-1} β (β β {0})) |
30 | 24, 28, 29 | mp2an 691 |
. . . . . . . 8
β’ {1, -1}
β (β β {0}) |
31 | | ressabs 17138 |
. . . . . . . 8
β’
(((β β {0}) β V β§ {1, -1} β (β β
{0})) β (((mulGrpββfld) βΎs
(β β {0})) βΎs {1, -1}) =
((mulGrpββfld) βΎs {1,
-1})) |
32 | 20, 30, 31 | mp2an 691 |
. . . . . . 7
β’
(((mulGrpββfld) βΎs (β
β {0})) βΎs {1, -1}) =
((mulGrpββfld) βΎs {1,
-1}) |
33 | 32 | eqcomi 2742 |
. . . . . 6
β’
((mulGrpββfld) βΎs {1, -1}) =
(((mulGrpββfld) βΎs (β β
{0})) βΎs {1, -1}) |
34 | | cnfldbas 20823 |
. . . . . . . 8
β’ β =
(Baseββfld) |
35 | | cnfld0 20844 |
. . . . . . . 8
β’ 0 =
(0gββfld) |
36 | | cndrng 20849 |
. . . . . . . 8
β’
βfld β DivRing |
37 | 34, 35, 36 | drngui 20225 |
. . . . . . 7
β’ (β
β {0}) = (Unitββfld) |
38 | | eqid 2733 |
. . . . . . 7
β’
(invrββfld) =
(invrββfld) |
39 | 37, 13, 38 | invrfval 20110 |
. . . . . 6
β’
(invrββfld) =
(invgβ((mulGrpββfld)
βΎs (β β {0}))) |
40 | 33, 39, 7 | subginv 18943 |
. . . . 5
β’ (({1, -1}
β (SubGrpβ((mulGrpββfld) βΎs
(β β {0}))) β§ (πβπΉ) β {1, -1}) β
((invrββfld)β(πβπΉ)) =
((invgβ((mulGrpββfld)
βΎs {1, -1}))β(πβπΉ))) |
41 | 14, 18, 40 | sylancr 588 |
. . . 4
β’ ((π· β Fin β§ πΉ β π) β
((invrββfld)β(πβπΉ)) =
((invgβ((mulGrpββfld)
βΎs {1, -1}))β(πβπΉ))) |
42 | 30, 18 | sselid 3946 |
. . . . . 6
β’ ((π· β Fin β§ πΉ β π) β (πβπΉ) β (β β
{0})) |
43 | | eldifsn 4751 |
. . . . . 6
β’ ((πβπΉ) β (β β {0}) β
((πβπΉ) β β β§ (πβπΉ) β 0)) |
44 | 42, 43 | sylib 217 |
. . . . 5
β’ ((π· β Fin β§ πΉ β π) β ((πβπΉ) β β β§ (πβπΉ) β 0)) |
45 | | cnfldinv 20851 |
. . . . 5
β’ (((πβπΉ) β β β§ (πβπΉ) β 0) β
((invrββfld)β(πβπΉ)) = (1 / (πβπΉ))) |
46 | 44, 45 | syl 17 |
. . . 4
β’ ((π· β Fin β§ πΉ β π) β
((invrββfld)β(πβπΉ)) = (1 / (πβπΉ))) |
47 | 41, 46 | eqtr3d 2775 |
. . 3
β’ ((π· β Fin β§ πΉ β π) β
((invgβ((mulGrpββfld)
βΎs {1, -1}))β(πβπΉ)) = (1 / (πβπΉ))) |
48 | 9, 12, 47 | 3eqtr3d 2781 |
. 2
β’ ((π· β Fin β§ πΉ β π) β (πββ‘πΉ) = (1 / (πβπΉ))) |
49 | | fvex 6859 |
. . . . 5
β’ (πβπΉ) β V |
50 | 49 | elpr 4613 |
. . . 4
β’ ((πβπΉ) β {1, -1} β ((πβπΉ) = 1 β¨ (πβπΉ) = -1)) |
51 | | 1div1e1 11853 |
. . . . . 6
β’ (1 / 1) =
1 |
52 | | oveq2 7369 |
. . . . . 6
β’ ((πβπΉ) = 1 β (1 / (πβπΉ)) = (1 / 1)) |
53 | | id 22 |
. . . . . 6
β’ ((πβπΉ) = 1 β (πβπΉ) = 1) |
54 | 51, 52, 53 | 3eqtr4a 2799 |
. . . . 5
β’ ((πβπΉ) = 1 β (1 / (πβπΉ)) = (πβπΉ)) |
55 | | divneg2 11887 |
. . . . . . . 8
β’ ((1
β β β§ 1 β β β§ 1 β 0) β -(1 / 1) = (1 /
-1)) |
56 | 21, 21, 22, 55 | mp3an 1462 |
. . . . . . 7
β’ -(1 / 1)
= (1 / -1) |
57 | 51 | negeqi 11402 |
. . . . . . 7
β’ -(1 / 1)
= -1 |
58 | 56, 57 | eqtr3i 2763 |
. . . . . 6
β’ (1 / -1)
= -1 |
59 | | oveq2 7369 |
. . . . . 6
β’ ((πβπΉ) = -1 β (1 / (πβπΉ)) = (1 / -1)) |
60 | | id 22 |
. . . . . 6
β’ ((πβπΉ) = -1 β (πβπΉ) = -1) |
61 | 58, 59, 60 | 3eqtr4a 2799 |
. . . . 5
β’ ((πβπΉ) = -1 β (1 / (πβπΉ)) = (πβπΉ)) |
62 | 54, 61 | jaoi 856 |
. . . 4
β’ (((πβπΉ) = 1 β¨ (πβπΉ) = -1) β (1 / (πβπΉ)) = (πβπΉ)) |
63 | 50, 62 | sylbi 216 |
. . 3
β’ ((πβπΉ) β {1, -1} β (1 / (πβπΉ)) = (πβπΉ)) |
64 | 18, 63 | syl 17 |
. 2
β’ ((π· β Fin β§ πΉ β π) β (1 / (πβπΉ)) = (πβπΉ)) |
65 | 48, 64 | eqtrd 2773 |
1
β’ ((π· β Fin β§ πΉ β π) β (πββ‘πΉ) = (πβπΉ)) |