Proof of Theorem psgninv
Step | Hyp | Ref
| Expression |
1 | | psgninv.s |
. . . . 5
⊢ 𝑆 = (SymGrp‘𝐷) |
2 | | psgninv.n |
. . . . 5
⊢ 𝑁 = (pmSgn‘𝐷) |
3 | | eqid 2622 |
. . . . 5
⊢
((mulGrp‘ℂfld) ↾s {1, -1}) =
((mulGrp‘ℂfld) ↾s {1,
-1}) |
4 | 1, 2, 3 | psgnghm2 19927 |
. . . 4
⊢ (𝐷 ∈ Fin → 𝑁 ∈ (𝑆 GrpHom
((mulGrp‘ℂfld) ↾s {1,
-1}))) |
5 | | psgninv.p |
. . . . 5
⊢ 𝑃 = (Base‘𝑆) |
6 | | eqid 2622 |
. . . . 5
⊢
(invg‘𝑆) = (invg‘𝑆) |
7 | | eqid 2622 |
. . . . 5
⊢
(invg‘((mulGrp‘ℂfld)
↾s {1, -1})) =
(invg‘((mulGrp‘ℂfld)
↾s {1, -1})) |
8 | 5, 6, 7 | ghminv 17667 |
. . . 4
⊢ ((𝑁 ∈ (𝑆 GrpHom
((mulGrp‘ℂfld) ↾s {1, -1})) ∧ 𝐹 ∈ 𝑃) → (𝑁‘((invg‘𝑆)‘𝐹)) =
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹))) |
9 | 4, 8 | sylan 488 |
. . 3
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘((invg‘𝑆)‘𝐹)) =
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹))) |
10 | 1, 5, 6 | symginv 17822 |
. . . . 5
⊢ (𝐹 ∈ 𝑃 → ((invg‘𝑆)‘𝐹) = ◡𝐹) |
11 | 10 | adantl 482 |
. . . 4
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → ((invg‘𝑆)‘𝐹) = ◡𝐹) |
12 | 11 | fveq2d 6195 |
. . 3
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘((invg‘𝑆)‘𝐹)) = (𝑁‘◡𝐹)) |
13 | | eqid 2622 |
. . . . . 6
⊢
((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
14 | 13 | cnmsgnsubg 19923 |
. . . . 5
⊢ {1, -1}
∈ (SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) |
15 | 3 | cnmsgnbas 19924 |
. . . . . . . 8
⊢ {1, -1} =
(Base‘((mulGrp‘ℂfld) ↾s {1,
-1})) |
16 | 5, 15 | ghmf 17664 |
. . . . . . 7
⊢ (𝑁 ∈ (𝑆 GrpHom
((mulGrp‘ℂfld) ↾s {1, -1})) →
𝑁:𝑃⟶{1, -1}) |
17 | 4, 16 | syl 17 |
. . . . . 6
⊢ (𝐷 ∈ Fin → 𝑁:𝑃⟶{1, -1}) |
18 | 17 | ffvelrnda 6359 |
. . . . 5
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘𝐹) ∈ {1, -1}) |
19 | | cnex 10017 |
. . . . . . . . 9
⊢ ℂ
∈ V |
20 | | difss 3737 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ⊆ ℂ |
21 | 19, 20 | ssexi 4803 |
. . . . . . . 8
⊢ (ℂ
∖ {0}) ∈ V |
22 | | ax-1cn 9994 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
23 | | ax-1ne0 10005 |
. . . . . . . . . 10
⊢ 1 ≠
0 |
24 | | eldifsn 4317 |
. . . . . . . . . 10
⊢ (1 ∈
(ℂ ∖ {0}) ↔ (1 ∈ ℂ ∧ 1 ≠
0)) |
25 | 22, 23, 24 | mpbir2an 955 |
. . . . . . . . 9
⊢ 1 ∈
(ℂ ∖ {0}) |
26 | | neg1cn 11124 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
27 | | neg1ne0 11126 |
. . . . . . . . . 10
⊢ -1 ≠
0 |
28 | | eldifsn 4317 |
. . . . . . . . . 10
⊢ (-1
∈ (ℂ ∖ {0}) ↔ (-1 ∈ ℂ ∧ -1 ≠
0)) |
29 | 26, 27, 28 | mpbir2an 955 |
. . . . . . . . 9
⊢ -1 ∈
(ℂ ∖ {0}) |
30 | | prssi 4353 |
. . . . . . . . 9
⊢ ((1
∈ (ℂ ∖ {0}) ∧ -1 ∈ (ℂ ∖ {0})) → {1,
-1} ⊆ (ℂ ∖ {0})) |
31 | 25, 29, 30 | mp2an 708 |
. . . . . . . 8
⊢ {1, -1}
⊆ (ℂ ∖ {0}) |
32 | | ressabs 15939 |
. . . . . . . 8
⊢
(((ℂ ∖ {0}) ∈ V ∧ {1, -1} ⊆ (ℂ ∖
{0})) → (((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) ↾s {1, -1}) =
((mulGrp‘ℂfld) ↾s {1,
-1})) |
33 | 21, 31, 32 | mp2an 708 |
. . . . . . 7
⊢
(((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) ↾s {1, -1}) =
((mulGrp‘ℂfld) ↾s {1,
-1}) |
34 | 33 | eqcomi 2631 |
. . . . . 6
⊢
((mulGrp‘ℂfld) ↾s {1, -1}) =
(((mulGrp‘ℂfld) ↾s (ℂ ∖
{0})) ↾s {1, -1}) |
35 | | cnfldbas 19750 |
. . . . . . . 8
⊢ ℂ =
(Base‘ℂfld) |
36 | | cnfld0 19770 |
. . . . . . . 8
⊢ 0 =
(0g‘ℂfld) |
37 | | cndrng 19775 |
. . . . . . . 8
⊢
ℂfld ∈ DivRing |
38 | 35, 36, 37 | drngui 18753 |
. . . . . . 7
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
39 | | eqid 2622 |
. . . . . . 7
⊢
(invr‘ℂfld) =
(invr‘ℂfld) |
40 | 38, 13, 39 | invrfval 18673 |
. . . . . 6
⊢
(invr‘ℂfld) =
(invg‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) |
41 | 34, 40, 7 | subginv 17601 |
. . . . 5
⊢ (({1, -1}
∈ (SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) ∧ (𝑁‘𝐹) ∈ {1, -1}) →
((invr‘ℂfld)‘(𝑁‘𝐹)) =
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹))) |
42 | 14, 18, 41 | sylancr 695 |
. . . 4
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) →
((invr‘ℂfld)‘(𝑁‘𝐹)) =
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹))) |
43 | 31, 18 | sseldi 3601 |
. . . . . 6
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘𝐹) ∈ (ℂ ∖
{0})) |
44 | | eldifsn 4317 |
. . . . . 6
⊢ ((𝑁‘𝐹) ∈ (ℂ ∖ {0}) ↔
((𝑁‘𝐹) ∈ ℂ ∧ (𝑁‘𝐹) ≠ 0)) |
45 | 43, 44 | sylib 208 |
. . . . 5
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → ((𝑁‘𝐹) ∈ ℂ ∧ (𝑁‘𝐹) ≠ 0)) |
46 | | cnfldinv 19777 |
. . . . 5
⊢ (((𝑁‘𝐹) ∈ ℂ ∧ (𝑁‘𝐹) ≠ 0) →
((invr‘ℂfld)‘(𝑁‘𝐹)) = (1 / (𝑁‘𝐹))) |
47 | 45, 46 | syl 17 |
. . . 4
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) →
((invr‘ℂfld)‘(𝑁‘𝐹)) = (1 / (𝑁‘𝐹))) |
48 | 42, 47 | eqtr3d 2658 |
. . 3
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) →
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹)) = (1 / (𝑁‘𝐹))) |
49 | 9, 12, 48 | 3eqtr3d 2664 |
. 2
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘◡𝐹) = (1 / (𝑁‘𝐹))) |
50 | | fvex 6201 |
. . . . 5
⊢ (𝑁‘𝐹) ∈ V |
51 | 50 | elpr 4198 |
. . . 4
⊢ ((𝑁‘𝐹) ∈ {1, -1} ↔ ((𝑁‘𝐹) = 1 ∨ (𝑁‘𝐹) = -1)) |
52 | | 1div1e1 10717 |
. . . . . 6
⊢ (1 / 1) =
1 |
53 | | oveq2 6658 |
. . . . . 6
⊢ ((𝑁‘𝐹) = 1 → (1 / (𝑁‘𝐹)) = (1 / 1)) |
54 | | id 22 |
. . . . . 6
⊢ ((𝑁‘𝐹) = 1 → (𝑁‘𝐹) = 1) |
55 | 52, 53, 54 | 3eqtr4a 2682 |
. . . . 5
⊢ ((𝑁‘𝐹) = 1 → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) |
56 | | divneg2 10749 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 /
-1)) |
57 | 22, 22, 23, 56 | mp3an 1424 |
. . . . . . 7
⊢ -(1 / 1)
= (1 / -1) |
58 | 52 | negeqi 10274 |
. . . . . . 7
⊢ -(1 / 1)
= -1 |
59 | 57, 58 | eqtr3i 2646 |
. . . . . 6
⊢ (1 / -1)
= -1 |
60 | | oveq2 6658 |
. . . . . 6
⊢ ((𝑁‘𝐹) = -1 → (1 / (𝑁‘𝐹)) = (1 / -1)) |
61 | | id 22 |
. . . . . 6
⊢ ((𝑁‘𝐹) = -1 → (𝑁‘𝐹) = -1) |
62 | 59, 60, 61 | 3eqtr4a 2682 |
. . . . 5
⊢ ((𝑁‘𝐹) = -1 → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) |
63 | 55, 62 | jaoi 394 |
. . . 4
⊢ (((𝑁‘𝐹) = 1 ∨ (𝑁‘𝐹) = -1) → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) |
64 | 51, 63 | sylbi 207 |
. . 3
⊢ ((𝑁‘𝐹) ∈ {1, -1} → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) |
65 | 18, 64 | syl 17 |
. 2
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) |
66 | 49, 65 | eqtrd 2656 |
1
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘◡𝐹) = (𝑁‘𝐹)) |