Step | Hyp | Ref
| Expression |
1 | | cnmsgnsubg.m |
. 2
โข ๐ =
((mulGrpโโfld) โพs (โ โ
{0})) |
2 | | elpri 4651 |
. . 3
โข (๐ฅ โ {1, -1} โ (๐ฅ = 1 โจ ๐ฅ = -1)) |
3 | | id 22 |
. . . . 5
โข (๐ฅ = 1 โ ๐ฅ = 1) |
4 | | ax-1cn 11171 |
. . . . 5
โข 1 โ
โ |
5 | 3, 4 | eqeltrdi 2840 |
. . . 4
โข (๐ฅ = 1 โ ๐ฅ โ โ) |
6 | | id 22 |
. . . . 5
โข (๐ฅ = -1 โ ๐ฅ = -1) |
7 | | neg1cn 12331 |
. . . . 5
โข -1 โ
โ |
8 | 6, 7 | eqeltrdi 2840 |
. . . 4
โข (๐ฅ = -1 โ ๐ฅ โ โ) |
9 | 5, 8 | jaoi 854 |
. . 3
โข ((๐ฅ = 1 โจ ๐ฅ = -1) โ ๐ฅ โ โ) |
10 | 2, 9 | syl 17 |
. 2
โข (๐ฅ โ {1, -1} โ ๐ฅ โ
โ) |
11 | | ax-1ne0 11182 |
. . . . . 6
โข 1 โ
0 |
12 | 11 | a1i 11 |
. . . . 5
โข (๐ฅ = 1 โ 1 โ
0) |
13 | 3, 12 | eqnetrd 3007 |
. . . 4
โข (๐ฅ = 1 โ ๐ฅ โ 0) |
14 | | neg1ne0 12333 |
. . . . . 6
โข -1 โ
0 |
15 | 14 | a1i 11 |
. . . . 5
โข (๐ฅ = -1 โ -1 โ
0) |
16 | 6, 15 | eqnetrd 3007 |
. . . 4
โข (๐ฅ = -1 โ ๐ฅ โ 0) |
17 | 13, 16 | jaoi 854 |
. . 3
โข ((๐ฅ = 1 โจ ๐ฅ = -1) โ ๐ฅ โ 0) |
18 | 2, 17 | syl 17 |
. 2
โข (๐ฅ โ {1, -1} โ ๐ฅ โ 0) |
19 | | elpri 4651 |
. . 3
โข (๐ฆ โ {1, -1} โ (๐ฆ = 1 โจ ๐ฆ = -1)) |
20 | | oveq12 7421 |
. . . . 5
โข ((๐ฅ = 1 โง ๐ฆ = 1) โ (๐ฅ ยท ๐ฆ) = (1 ยท 1)) |
21 | 4 | mulridi 11223 |
. . . . . 6
โข (1
ยท 1) = 1 |
22 | | 1ex 11215 |
. . . . . . 7
โข 1 โ
V |
23 | 22 | prid1 4767 |
. . . . . 6
โข 1 โ
{1, -1} |
24 | 21, 23 | eqeltri 2828 |
. . . . 5
โข (1
ยท 1) โ {1, -1} |
25 | 20, 24 | eqeltrdi 2840 |
. . . 4
โข ((๐ฅ = 1 โง ๐ฆ = 1) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
26 | | oveq12 7421 |
. . . . 5
โข ((๐ฅ = -1 โง ๐ฆ = 1) โ (๐ฅ ยท ๐ฆ) = (-1 ยท 1)) |
27 | 7 | mulridi 11223 |
. . . . . 6
โข (-1
ยท 1) = -1 |
28 | | negex 11463 |
. . . . . . 7
โข -1 โ
V |
29 | 28 | prid2 4768 |
. . . . . 6
โข -1 โ
{1, -1} |
30 | 27, 29 | eqeltri 2828 |
. . . . 5
โข (-1
ยท 1) โ {1, -1} |
31 | 26, 30 | eqeltrdi 2840 |
. . . 4
โข ((๐ฅ = -1 โง ๐ฆ = 1) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
32 | | oveq12 7421 |
. . . . 5
โข ((๐ฅ = 1 โง ๐ฆ = -1) โ (๐ฅ ยท ๐ฆ) = (1 ยท -1)) |
33 | 7 | mullidi 11224 |
. . . . . 6
โข (1
ยท -1) = -1 |
34 | 33, 29 | eqeltri 2828 |
. . . . 5
โข (1
ยท -1) โ {1, -1} |
35 | 32, 34 | eqeltrdi 2840 |
. . . 4
โข ((๐ฅ = 1 โง ๐ฆ = -1) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
36 | | oveq12 7421 |
. . . . 5
โข ((๐ฅ = -1 โง ๐ฆ = -1) โ (๐ฅ ยท ๐ฆ) = (-1 ยท -1)) |
37 | | neg1mulneg1e1 12430 |
. . . . . 6
โข (-1
ยท -1) = 1 |
38 | 37, 23 | eqeltri 2828 |
. . . . 5
โข (-1
ยท -1) โ {1, -1} |
39 | 36, 38 | eqeltrdi 2840 |
. . . 4
โข ((๐ฅ = -1 โง ๐ฆ = -1) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
40 | 25, 31, 35, 39 | ccase 1035 |
. . 3
โข (((๐ฅ = 1 โจ ๐ฅ = -1) โง (๐ฆ = 1 โจ ๐ฆ = -1)) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
41 | 2, 19, 40 | syl2an 595 |
. 2
โข ((๐ฅ โ {1, -1} โง ๐ฆ โ {1, -1}) โ (๐ฅ ยท ๐ฆ) โ {1, -1}) |
42 | | oveq2 7420 |
. . . . 5
โข (๐ฅ = 1 โ (1 / ๐ฅ) = (1 / 1)) |
43 | | 1div1e1 11909 |
. . . . . 6
โข (1 / 1) =
1 |
44 | 43, 23 | eqeltri 2828 |
. . . . 5
โข (1 / 1)
โ {1, -1} |
45 | 42, 44 | eqeltrdi 2840 |
. . . 4
โข (๐ฅ = 1 โ (1 / ๐ฅ) โ {1,
-1}) |
46 | | oveq2 7420 |
. . . . 5
โข (๐ฅ = -1 โ (1 / ๐ฅ) = (1 / -1)) |
47 | | divneg2 11943 |
. . . . . . . 8
โข ((1
โ โ โง 1 โ โ โง 1 โ 0) โ -(1 / 1) = (1 /
-1)) |
48 | 4, 4, 11, 47 | mp3an 1460 |
. . . . . . 7
โข -(1 / 1)
= (1 / -1) |
49 | 43 | negeqi 11458 |
. . . . . . 7
โข -(1 / 1)
= -1 |
50 | 48, 49 | eqtr3i 2761 |
. . . . . 6
โข (1 / -1)
= -1 |
51 | 50, 29 | eqeltri 2828 |
. . . . 5
โข (1 / -1)
โ {1, -1} |
52 | 46, 51 | eqeltrdi 2840 |
. . . 4
โข (๐ฅ = -1 โ (1 / ๐ฅ) โ {1,
-1}) |
53 | 45, 52 | jaoi 854 |
. . 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 21209 |
1
โข {1, -1}
โ (SubGrpโ๐) |