Step | Hyp | Ref
| Expression |
1 | | 2zrng.e |
. . 3
โข ๐ธ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ)} |
2 | | 2zrngbas.r |
. . 3
โข ๐
= (โfld
โพs ๐ธ) |
3 | 1, 2 | 2zrngamnd 46829 |
. 2
โข ๐
โ Mnd |
4 | | eqeq1 2736 |
. . . . . . 7
โข (๐ง = ๐ฆ โ (๐ง = (2 ยท ๐ฅ) โ ๐ฆ = (2 ยท ๐ฅ))) |
5 | 4 | rexbidv 3178 |
. . . . . 6
โข (๐ง = ๐ฆ โ (โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ) โ โ๐ฅ โ โค ๐ฆ = (2 ยท ๐ฅ))) |
6 | 5, 1 | elrab2 3686 |
. . . . 5
โข (๐ฆ โ ๐ธ โ (๐ฆ โ โค โง โ๐ฅ โ โค ๐ฆ = (2 ยท ๐ฅ))) |
7 | | znegcl 12596 |
. . . . . . 7
โข (๐ฆ โ โค โ -๐ฆ โ
โค) |
8 | 7 | adantr 481 |
. . . . . 6
โข ((๐ฆ โ โค โง
โ๐ฅ โ โค
๐ฆ = (2 ยท ๐ฅ)) โ -๐ฆ โ โค) |
9 | | nfv 1917 |
. . . . . . . 8
โข
โฒ๐ฅ ๐ฆ โ โค |
10 | | nfre1 3282 |
. . . . . . . 8
โข
โฒ๐ฅโ๐ฅ โ โค -๐ฆ = (2 ยท ๐ฅ) |
11 | | znegcl 12596 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โค โ -๐ฅ โ
โค) |
12 | 11 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โค โง ๐ฅ โ โค) โ -๐ฅ โ
โค) |
13 | 12 | adantr 481 |
. . . . . . . . . . 11
โข (((๐ฆ โ โค โง ๐ฅ โ โค) โง ๐ฆ = (2 ยท ๐ฅ)) โ -๐ฅ โ โค) |
14 | | oveq2 7416 |
. . . . . . . . . . . . 13
โข (๐ง = -๐ฅ โ (2 ยท ๐ง) = (2 ยท -๐ฅ)) |
15 | 14 | eqeq2d 2743 |
. . . . . . . . . . . 12
โข (๐ง = -๐ฅ โ (-๐ฆ = (2 ยท ๐ง) โ -๐ฆ = (2 ยท -๐ฅ))) |
16 | 15 | adantl 482 |
. . . . . . . . . . 11
โข ((((๐ฆ โ โค โง ๐ฅ โ โค) โง ๐ฆ = (2 ยท ๐ฅ)) โง ๐ง = -๐ฅ) โ (-๐ฆ = (2 ยท ๐ง) โ -๐ฆ = (2 ยท -๐ฅ))) |
17 | | negeq 11451 |
. . . . . . . . . . . 12
โข (๐ฆ = (2 ยท ๐ฅ) โ -๐ฆ = -(2 ยท ๐ฅ)) |
18 | | 2cnd 12289 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ 2 โ
โ) |
19 | | zcn 12562 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
20 | 18, 19 | mulneg2d 11667 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โค โ (2
ยท -๐ฅ) = -(2 ยท
๐ฅ)) |
21 | 20 | eqcomd 2738 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โค โ -(2
ยท ๐ฅ) = (2 ยท
-๐ฅ)) |
22 | 21 | adantl 482 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โค โง ๐ฅ โ โค) โ -(2
ยท ๐ฅ) = (2 ยท
-๐ฅ)) |
23 | 17, 22 | sylan9eqr 2794 |
. . . . . . . . . . 11
โข (((๐ฆ โ โค โง ๐ฅ โ โค) โง ๐ฆ = (2 ยท ๐ฅ)) โ -๐ฆ = (2 ยท -๐ฅ)) |
24 | 13, 16, 23 | rspcedvd 3614 |
. . . . . . . . . 10
โข (((๐ฆ โ โค โง ๐ฅ โ โค) โง ๐ฆ = (2 ยท ๐ฅ)) โ โ๐ง โ โค -๐ฆ = (2 ยท ๐ง)) |
25 | | oveq2 7416 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ง โ (2 ยท ๐ฅ) = (2 ยท ๐ง)) |
26 | 25 | eqeq2d 2743 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ง โ (-๐ฆ = (2 ยท ๐ฅ) โ -๐ฆ = (2 ยท ๐ง))) |
27 | 26 | cbvrexvw 3235 |
. . . . . . . . . 10
โข
(โ๐ฅ โ
โค -๐ฆ = (2 ยท
๐ฅ) โ โ๐ง โ โค -๐ฆ = (2 ยท ๐ง)) |
28 | 24, 27 | sylibr 233 |
. . . . . . . . 9
โข (((๐ฆ โ โค โง ๐ฅ โ โค) โง ๐ฆ = (2 ยท ๐ฅ)) โ โ๐ฅ โ โค -๐ฆ = (2 ยท ๐ฅ)) |
29 | 28 | exp31 420 |
. . . . . . . 8
โข (๐ฆ โ โค โ (๐ฅ โ โค โ (๐ฆ = (2 ยท ๐ฅ) โ โ๐ฅ โ โค -๐ฆ = (2 ยท ๐ฅ)))) |
30 | 9, 10, 29 | rexlimd 3263 |
. . . . . . 7
โข (๐ฆ โ โค โ
(โ๐ฅ โ โค
๐ฆ = (2 ยท ๐ฅ) โ โ๐ฅ โ โค -๐ฆ = (2 ยท ๐ฅ))) |
31 | 30 | imp 407 |
. . . . . 6
โข ((๐ฆ โ โค โง
โ๐ฅ โ โค
๐ฆ = (2 ยท ๐ฅ)) โ โ๐ฅ โ โค -๐ฆ = (2 ยท ๐ฅ)) |
32 | | eqeq1 2736 |
. . . . . . . 8
โข (๐ง = -๐ฆ โ (๐ง = (2 ยท ๐ฅ) โ -๐ฆ = (2 ยท ๐ฅ))) |
33 | 32 | rexbidv 3178 |
. . . . . . 7
โข (๐ง = -๐ฆ โ (โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ) โ โ๐ฅ โ โค -๐ฆ = (2 ยท ๐ฅ))) |
34 | 33, 1 | elrab2 3686 |
. . . . . 6
โข (-๐ฆ โ ๐ธ โ (-๐ฆ โ โค โง โ๐ฅ โ โค -๐ฆ = (2 ยท ๐ฅ))) |
35 | 8, 31, 34 | sylanbrc 583 |
. . . . 5
โข ((๐ฆ โ โค โง
โ๐ฅ โ โค
๐ฆ = (2 ยท ๐ฅ)) โ -๐ฆ โ ๐ธ) |
36 | 6, 35 | sylbi 216 |
. . . 4
โข (๐ฆ โ ๐ธ โ -๐ฆ โ ๐ธ) |
37 | | oveq1 7415 |
. . . . . 6
โข (๐ง = -๐ฆ โ (๐ง + ๐ฆ) = (-๐ฆ + ๐ฆ)) |
38 | 37 | eqeq1d 2734 |
. . . . 5
โข (๐ง = -๐ฆ โ ((๐ง + ๐ฆ) = 0 โ (-๐ฆ + ๐ฆ) = 0)) |
39 | 38 | adantl 482 |
. . . 4
โข ((๐ฆ โ ๐ธ โง ๐ง = -๐ฆ) โ ((๐ง + ๐ฆ) = 0 โ (-๐ฆ + ๐ฆ) = 0)) |
40 | | elrabi 3677 |
. . . . . . . . 9
โข (๐ฆ โ {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ)} โ ๐ฆ โ โค) |
41 | 40, 1 | eleq2s 2851 |
. . . . . . . 8
โข (๐ฆ โ ๐ธ โ ๐ฆ โ โค) |
42 | 41 | zcnd 12666 |
. . . . . . 7
โข (๐ฆ โ ๐ธ โ ๐ฆ โ โ) |
43 | 42 | negcld 11557 |
. . . . . 6
โข (๐ฆ โ ๐ธ โ -๐ฆ โ โ) |
44 | 43, 42 | addcomd 11415 |
. . . . 5
โข (๐ฆ โ ๐ธ โ (-๐ฆ + ๐ฆ) = (๐ฆ + -๐ฆ)) |
45 | 42 | negidd 11560 |
. . . . 5
โข (๐ฆ โ ๐ธ โ (๐ฆ + -๐ฆ) = 0) |
46 | 44, 45 | eqtrd 2772 |
. . . 4
โข (๐ฆ โ ๐ธ โ (-๐ฆ + ๐ฆ) = 0) |
47 | 36, 39, 46 | rspcedvd 3614 |
. . 3
โข (๐ฆ โ ๐ธ โ โ๐ง โ ๐ธ (๐ง + ๐ฆ) = 0) |
48 | 47 | rgen 3063 |
. 2
โข
โ๐ฆ โ
๐ธ โ๐ง โ ๐ธ (๐ง + ๐ฆ) = 0 |
49 | 1, 2 | 2zrngbas 46824 |
. . 3
โข ๐ธ = (Baseโ๐
) |
50 | 1, 2 | 2zrngadd 46825 |
. . 3
โข + =
(+gโ๐
) |
51 | 1, 2 | 2zrng0 46826 |
. . 3
โข 0 =
(0gโ๐
) |
52 | 49, 50, 51 | isgrp 18824 |
. 2
โข (๐
โ Grp โ (๐
โ Mnd โง โ๐ฆ โ ๐ธ โ๐ง โ ๐ธ (๐ง + ๐ฆ) = 0)) |
53 | 3, 48, 52 | mpbir2an 709 |
1
โข ๐
โ Grp |