Metamath Proof Explorer

Theorem cnmsgngrp

Description: The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015)

Ref Expression
Hypothesis cnmsgngrp.u ⊢ U = mulGrp ℂ fld ↾ 𝑠 1 − 1
Assertion cnmsgngrp ⊢ U ∈ Grp

Proof

Step Hyp Ref Expression
1 cnmsgngrp.u ⊢ U = mulGrp ℂ fld ↾ 𝑠 1 − 1
2 eqid ⊢ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 = mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
3 2 cnmsgnsubg ⊢ 1 − 1 ∈ SubGrp ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0
4 cnex ⊢ ℂ ∈ V
5 4 difexi ⊢ ℂ ∖ 0 ∈ V
6 ax-1cn ⊢ 1 ∈ ℂ
7 ax-1ne0 ⊢ 1 ≠ 0
8 eldifsn ⊢ 1 ∈ ℂ ∖ 0 ↔ 1 ∈ ℂ ∧ 1 ≠ 0
9 6 7 8 mpbir2an ⊢ 1 ∈ ℂ ∖ 0
10 neg1cn ⊢ − 1 ∈ ℂ
11 neg1ne0 ⊢ − 1 ≠ 0
12 eldifsn ⊢ − 1 ∈ ℂ ∖ 0 ↔ − 1 ∈ ℂ ∧ − 1 ≠ 0
13 10 11 12 mpbir2an ⊢ − 1 ∈ ℂ ∖ 0
14 prssi ⊢ 1 ∈ ℂ ∖ 0 ∧ − 1 ∈ ℂ ∖ 0 → 1 − 1 ⊆ ℂ ∖ 0
15 9 13 14 mp2an ⊢ 1 − 1 ⊆ ℂ ∖ 0
16 ressabs ⊢ ℂ ∖ 0 ∈ V ∧ 1 − 1 ⊆ ℂ ∖ 0 → mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
17 5 15 16 mp2an ⊢ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ↾ 𝑠 1 − 1 = mulGrp ℂ fld ↾ 𝑠 1 − 1
18 1 17 eqtr4i ⊢ U = mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 ↾ 𝑠 1 − 1
19 18 subggrp ⊢ 1 − 1 ∈ SubGrp ⁡ mulGrp ℂ fld ↾ 𝑠 ℂ ∖ 0 → U ∈ Grp
20 3 19 ax-mp ⊢ U ∈ Grp