Proof of Theorem psgninv
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | psgninv.s | . . . . 5
⊢ 𝑆 = (SymGrp‘𝐷) | 
| 2 |  | psgninv.n | . . . . 5
⊢ 𝑁 = (pmSgn‘𝐷) | 
| 3 |  | eqid 2737 | . . . . 5
⊢
((mulGrp‘ℂfld) ↾s {1, -1}) =
((mulGrp‘ℂfld) ↾s {1,
-1}) | 
| 4 | 1, 2, 3 | psgnghm2 21599 | . . . 4
⊢ (𝐷 ∈ Fin → 𝑁 ∈ (𝑆 GrpHom
((mulGrp‘ℂfld) ↾s {1,
-1}))) | 
| 5 |  | psgninv.p | . . . . 5
⊢ 𝑃 = (Base‘𝑆) | 
| 6 |  | eqid 2737 | . . . . 5
⊢
(invg‘𝑆) = (invg‘𝑆) | 
| 7 |  | eqid 2737 | . . . . 5
⊢
(invg‘((mulGrp‘ℂfld)
↾s {1, -1})) =
(invg‘((mulGrp‘ℂfld)
↾s {1, -1})) | 
| 8 | 5, 6, 7 | ghminv 19241 | . . . 4
⊢ ((𝑁 ∈ (𝑆 GrpHom
((mulGrp‘ℂfld) ↾s {1, -1})) ∧ 𝐹 ∈ 𝑃) → (𝑁‘((invg‘𝑆)‘𝐹)) =
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹))) | 
| 9 | 4, 8 | sylan 580 | . . 3
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘((invg‘𝑆)‘𝐹)) =
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹))) | 
| 10 | 1, 5, 6 | symginv 19420 | . . . . 5
⊢ (𝐹 ∈ 𝑃 → ((invg‘𝑆)‘𝐹) = ◡𝐹) | 
| 11 | 10 | adantl 481 | . . . 4
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → ((invg‘𝑆)‘𝐹) = ◡𝐹) | 
| 12 | 11 | fveq2d 6910 | . . 3
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘((invg‘𝑆)‘𝐹)) = (𝑁‘◡𝐹)) | 
| 13 |  | eqid 2737 | . . . . . 6
⊢
((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) | 
| 14 | 13 | cnmsgnsubg 21595 | . . . . 5
⊢ {1, -1}
∈ (SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) | 
| 15 | 3 | cnmsgnbas 21596 | . . . . . . . 8
⊢ {1, -1} =
(Base‘((mulGrp‘ℂfld) ↾s {1,
-1})) | 
| 16 | 5, 15 | ghmf 19238 | . . . . . . 7
⊢ (𝑁 ∈ (𝑆 GrpHom
((mulGrp‘ℂfld) ↾s {1, -1})) →
𝑁:𝑃⟶{1, -1}) | 
| 17 | 4, 16 | syl 17 | . . . . . 6
⊢ (𝐷 ∈ Fin → 𝑁:𝑃⟶{1, -1}) | 
| 18 | 17 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘𝐹) ∈ {1, -1}) | 
| 19 |  | cnex 11236 | . . . . . . . . 9
⊢ ℂ
∈ V | 
| 20 | 19 | difexi 5330 | . . . . . . . 8
⊢ (ℂ
∖ {0}) ∈ V | 
| 21 |  | ax-1cn 11213 | . . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 22 |  | ax-1ne0 11224 | . . . . . . . . . 10
⊢ 1 ≠
0 | 
| 23 |  | eldifsn 4786 | . . . . . . . . . 10
⊢ (1 ∈
(ℂ ∖ {0}) ↔ (1 ∈ ℂ ∧ 1 ≠
0)) | 
| 24 | 21, 22, 23 | mpbir2an 711 | . . . . . . . . 9
⊢ 1 ∈
(ℂ ∖ {0}) | 
| 25 |  | neg1cn 12380 | . . . . . . . . . 10
⊢ -1 ∈
ℂ | 
| 26 |  | neg1ne0 12382 | . . . . . . . . . 10
⊢ -1 ≠
0 | 
| 27 |  | eldifsn 4786 | . . . . . . . . . 10
⊢ (-1
∈ (ℂ ∖ {0}) ↔ (-1 ∈ ℂ ∧ -1 ≠
0)) | 
| 28 | 25, 26, 27 | mpbir2an 711 | . . . . . . . . 9
⊢ -1 ∈
(ℂ ∖ {0}) | 
| 29 |  | prssi 4821 | . . . . . . . . 9
⊢ ((1
∈ (ℂ ∖ {0}) ∧ -1 ∈ (ℂ ∖ {0})) → {1,
-1} ⊆ (ℂ ∖ {0})) | 
| 30 | 24, 28, 29 | mp2an 692 | . . . . . . . 8
⊢ {1, -1}
⊆ (ℂ ∖ {0}) | 
| 31 |  | ressabs 17294 | . . . . . . . 8
⊢
(((ℂ ∖ {0}) ∈ V ∧ {1, -1} ⊆ (ℂ ∖
{0})) → (((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) ↾s {1, -1}) =
((mulGrp‘ℂfld) ↾s {1,
-1})) | 
| 32 | 20, 30, 31 | mp2an 692 | . . . . . . 7
⊢
(((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) ↾s {1, -1}) =
((mulGrp‘ℂfld) ↾s {1,
-1}) | 
| 33 | 32 | eqcomi 2746 | . . . . . 6
⊢
((mulGrp‘ℂfld) ↾s {1, -1}) =
(((mulGrp‘ℂfld) ↾s (ℂ ∖
{0})) ↾s {1, -1}) | 
| 34 |  | cnfldbas 21368 | . . . . . . . 8
⊢ ℂ =
(Base‘ℂfld) | 
| 35 |  | cnfld0 21405 | . . . . . . . 8
⊢ 0 =
(0g‘ℂfld) | 
| 36 |  | cndrng 21411 | . . . . . . . 8
⊢
ℂfld ∈ DivRing | 
| 37 | 34, 35, 36 | drngui 20735 | . . . . . . 7
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) | 
| 38 |  | eqid 2737 | . . . . . . 7
⊢
(invr‘ℂfld) =
(invr‘ℂfld) | 
| 39 | 37, 13, 38 | invrfval 20389 | . . . . . 6
⊢
(invr‘ℂfld) =
(invg‘((mulGrp‘ℂfld)
↾s (ℂ ∖ {0}))) | 
| 40 | 33, 39, 7 | subginv 19151 | . . . . 5
⊢ (({1, -1}
∈ (SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) ∧ (𝑁‘𝐹) ∈ {1, -1}) →
((invr‘ℂfld)‘(𝑁‘𝐹)) =
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹))) | 
| 41 | 14, 18, 40 | sylancr 587 | . . . 4
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) →
((invr‘ℂfld)‘(𝑁‘𝐹)) =
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹))) | 
| 42 | 30, 18 | sselid 3981 | . . . . . 6
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘𝐹) ∈ (ℂ ∖
{0})) | 
| 43 |  | eldifsn 4786 | . . . . . 6
⊢ ((𝑁‘𝐹) ∈ (ℂ ∖ {0}) ↔
((𝑁‘𝐹) ∈ ℂ ∧ (𝑁‘𝐹) ≠ 0)) | 
| 44 | 42, 43 | sylib 218 | . . . . 5
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → ((𝑁‘𝐹) ∈ ℂ ∧ (𝑁‘𝐹) ≠ 0)) | 
| 45 |  | cnfldinv 21415 | . . . . 5
⊢ (((𝑁‘𝐹) ∈ ℂ ∧ (𝑁‘𝐹) ≠ 0) →
((invr‘ℂfld)‘(𝑁‘𝐹)) = (1 / (𝑁‘𝐹))) | 
| 46 | 44, 45 | syl 17 | . . . 4
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) →
((invr‘ℂfld)‘(𝑁‘𝐹)) = (1 / (𝑁‘𝐹))) | 
| 47 | 41, 46 | eqtr3d 2779 | . . 3
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) →
((invg‘((mulGrp‘ℂfld)
↾s {1, -1}))‘(𝑁‘𝐹)) = (1 / (𝑁‘𝐹))) | 
| 48 | 9, 12, 47 | 3eqtr3d 2785 | . 2
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘◡𝐹) = (1 / (𝑁‘𝐹))) | 
| 49 |  | fvex 6919 | . . . . 5
⊢ (𝑁‘𝐹) ∈ V | 
| 50 | 49 | elpr 4650 | . . . 4
⊢ ((𝑁‘𝐹) ∈ {1, -1} ↔ ((𝑁‘𝐹) = 1 ∨ (𝑁‘𝐹) = -1)) | 
| 51 |  | 1div1e1 11958 | . . . . . 6
⊢ (1 / 1) =
1 | 
| 52 |  | oveq2 7439 | . . . . . 6
⊢ ((𝑁‘𝐹) = 1 → (1 / (𝑁‘𝐹)) = (1 / 1)) | 
| 53 |  | id 22 | . . . . . 6
⊢ ((𝑁‘𝐹) = 1 → (𝑁‘𝐹) = 1) | 
| 54 | 51, 52, 53 | 3eqtr4a 2803 | . . . . 5
⊢ ((𝑁‘𝐹) = 1 → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) | 
| 55 |  | divneg2 11991 | . . . . . . . 8
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ ∧ 1 ≠ 0) → -(1 / 1) = (1 /
-1)) | 
| 56 | 21, 21, 22, 55 | mp3an 1463 | . . . . . . 7
⊢ -(1 / 1)
= (1 / -1) | 
| 57 | 51 | negeqi 11501 | . . . . . . 7
⊢ -(1 / 1)
= -1 | 
| 58 | 56, 57 | eqtr3i 2767 | . . . . . 6
⊢ (1 / -1)
= -1 | 
| 59 |  | oveq2 7439 | . . . . . 6
⊢ ((𝑁‘𝐹) = -1 → (1 / (𝑁‘𝐹)) = (1 / -1)) | 
| 60 |  | id 22 | . . . . . 6
⊢ ((𝑁‘𝐹) = -1 → (𝑁‘𝐹) = -1) | 
| 61 | 58, 59, 60 | 3eqtr4a 2803 | . . . . 5
⊢ ((𝑁‘𝐹) = -1 → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) | 
| 62 | 54, 61 | jaoi 858 | . . . 4
⊢ (((𝑁‘𝐹) = 1 ∨ (𝑁‘𝐹) = -1) → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) | 
| 63 | 50, 62 | sylbi 217 | . . 3
⊢ ((𝑁‘𝐹) ∈ {1, -1} → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) | 
| 64 | 18, 63 | syl 17 | . 2
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (1 / (𝑁‘𝐹)) = (𝑁‘𝐹)) | 
| 65 | 48, 64 | eqtrd 2777 | 1
⊢ ((𝐷 ∈ Fin ∧ 𝐹 ∈ 𝑃) → (𝑁‘◡𝐹) = (𝑁‘𝐹)) |