Step | Hyp | Ref
| Expression |
1 | | cnmsgnsubg.m |
. 2
โข ๐ =
((mulGrpโโfld) โพs (โ โ
{0})) |
2 | | elpri 4588 |
. . 3
โข (๐ฅ โ {1, -1} โ (๐ฅ = 1 โจ ๐ฅ = -1)) |
3 | | id 22 |
. . . . 5
โข (๐ฅ = 1 โ ๐ฅ = 1) |
4 | | ax-1cn 10972 |
. . . . 5
โข 1 โ
โ |
5 | 3, 4 | eqeltrdi 2845 |
. . . 4
โข (๐ฅ = 1 โ ๐ฅ โ โ) |
6 | | id 22 |
. . . . 5
โข (๐ฅ = -1 โ ๐ฅ = -1) |
7 | | neg1cn 12130 |
. . . . 5
โข -1 โ
โ |
8 | 6, 7 | eqeltrdi 2845 |
. . . 4
โข (๐ฅ = -1 โ ๐ฅ โ โ) |
9 | 5, 8 | jaoi 855 |
. . 3
โข ((๐ฅ = 1 โจ ๐ฅ = -1) โ ๐ฅ โ โ) |
10 | 2, 9 | syl 17 |
. 2
โข (๐ฅ โ {1, -1} โ ๐ฅ โ
โ) |
11 | | ax-1ne0 10983 |
. . . . . 6
โข 1 โ
0 |
12 | 11 | a1i 11 |
. . . . 5
โข (๐ฅ = 1 โ 1 โ
0) |
13 | 3, 12 | eqnetrd 3009 |
. . . 4
โข (๐ฅ = 1 โ ๐ฅ โ 0) |
14 | | neg1ne0 12132 |
. . . . . 6
โข -1 โ
0 |
15 | 14 | a1i 11 |
. . . . 5
โข (๐ฅ = -1 โ -1 โ
0) |
16 | 6, 15 | eqnetrd 3009 |
. . . 4
โข (๐ฅ = -1 โ ๐ฅ โ 0) |
17 | 13, 16 | jaoi 855 |
. . 3
โข ((๐ฅ = 1 โจ ๐ฅ = -1) โ ๐ฅ โ 0) |
18 | 2, 17 | syl 17 |
. 2
โข (๐ฅ โ {1, -1} โ ๐ฅ โ 0) |
19 | | elpri 4588 |
. . 3
โข (๐ฆ โ {1, -1} โ (๐ฆ = 1 โจ ๐ฆ = -1)) |
20 | | oveq12 7313 |
. . . . 5
โข ((๐ฅ = 1 โง ๐ฆ = 1) โ (๐ฅ ยท ๐ฆ) = (1 ยท 1)) |
21 | 4 | mulid1i 11022 |
. . . . . 6
โข (1
ยท 1) = 1 |
22 | | 1ex 11014 |
. . . . . . 7
โข 1 โ
V |
23 | 22 | prid1 4703 |
. . . . . 6
โข 1 โ
{1, -1} |
24 | 21, 23 | eqeltri 2833 |
. . . . 5
โข (1
ยท 1) โ {1, -1} |
25 | 20, 24 | eqeltrdi 2845 |
. . . 4
โข ((๐ฅ = 1 โง ๐ฆ = 1) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
26 | | oveq12 7313 |
. . . . 5
โข ((๐ฅ = -1 โง ๐ฆ = 1) โ (๐ฅ ยท ๐ฆ) = (-1 ยท 1)) |
27 | 7 | mulid1i 11022 |
. . . . . 6
โข (-1
ยท 1) = -1 |
28 | | negex 11262 |
. . . . . . 7
โข -1 โ
V |
29 | 28 | prid2 4704 |
. . . . . 6
โข -1 โ
{1, -1} |
30 | 27, 29 | eqeltri 2833 |
. . . . 5
โข (-1
ยท 1) โ {1, -1} |
31 | 26, 30 | eqeltrdi 2845 |
. . . 4
โข ((๐ฅ = -1 โง ๐ฆ = 1) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
32 | | oveq12 7313 |
. . . . 5
โข ((๐ฅ = 1 โง ๐ฆ = -1) โ (๐ฅ ยท ๐ฆ) = (1 ยท -1)) |
33 | 7 | mulid2i 11023 |
. . . . . 6
โข (1
ยท -1) = -1 |
34 | 33, 29 | eqeltri 2833 |
. . . . 5
โข (1
ยท -1) โ {1, -1} |
35 | 32, 34 | eqeltrdi 2845 |
. . . 4
โข ((๐ฅ = 1 โง ๐ฆ = -1) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
36 | | oveq12 7313 |
. . . . 5
โข ((๐ฅ = -1 โง ๐ฆ = -1) โ (๐ฅ ยท ๐ฆ) = (-1 ยท -1)) |
37 | | neg1mulneg1e1 12229 |
. . . . . 6
โข (-1
ยท -1) = 1 |
38 | 37, 23 | eqeltri 2833 |
. . . . 5
โข (-1
ยท -1) โ {1, -1} |
39 | 36, 38 | eqeltrdi 2845 |
. . . 4
โข ((๐ฅ = -1 โง ๐ฆ = -1) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
40 | 25, 31, 35, 39 | ccase 1036 |
. . 3
โข (((๐ฅ = 1 โจ ๐ฅ = -1) โง (๐ฆ = 1 โจ ๐ฆ = -1)) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
41 | 2, 19, 40 | syl2an 597 |
. 2
โข ((๐ฅ โ {1, -1} โง ๐ฆ โ {1, -1}) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
42 | | oveq2 7312 |
. . . . 5
โข (๐ฅ = 1 โ (1 / ๐ฅ) = (1 / 1)) |
43 | | 1div1e1 11708 |
. . . . . 6
โข (1 / 1) =
1 |
44 | 43, 23 | eqeltri 2833 |
. . . . 5
โข (1 / 1)
โ {1, -1} |
45 | 42, 44 | eqeltrdi 2845 |
. . . 4
โข (๐ฅ = 1 โ (1 / ๐ฅ) โ {1,
-1}) |
46 | | oveq2 7312 |
. . . . 5
โข (๐ฅ = -1 โ (1 / ๐ฅ) = (1 / -1)) |
47 | | divneg2 11742 |
. . . . . . . 8
โข ((1
โ โ โง 1 โ โ โง 1 โ 0) โ -(1 / 1) = (1 /
-1)) |
48 | 4, 4, 11, 47 | mp3an 1461 |
. . . . . . 7
โข -(1 / 1)
= (1 / -1) |
49 | 43 | negeqi 11257 |
. . . . . . 7
โข -(1 / 1)
= -1 |
50 | 48, 49 | eqtr3i 2766 |
. . . . . 6
โข (1 / -1)
= -1 |
51 | 50, 29 | eqeltri 2833 |
. . . . 5
โข (1 / -1)
โ {1, -1} |
52 | 46, 51 | eqeltrdi 2845 |
. . . 4
โข (๐ฅ = -1 โ (1 / ๐ฅ) โ {1,
-1}) |
53 | 45, 52 | jaoi 855 |
. . 3
โข ((๐ฅ = 1 โจ ๐ฅ = -1) โ (1 / ๐ฅ) โ {1, -1}) |
54 | 2, 53 | syl 17 |
. 2
โข (๐ฅ โ {1, -1} โ (1 /
๐ฅ) โ {1,
-1}) |
55 | 1, 10, 18, 41, 23, 54 | cnmsubglem 20703 |
1
โข {1, -1}
โ (SubGrpโ๐) |