Step | Hyp | Ref
| Expression |
1 | | eqeq1 2737 |
. . . . . 6
โข (๐ง = ๐ โ (๐ง = (2 ยท ๐ฅ) โ ๐ = (2 ยท ๐ฅ))) |
2 | 1 | rexbidv 3179 |
. . . . 5
โข (๐ง = ๐ โ (โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ) โ โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) |
3 | | 2zrng.e |
. . . . 5
โข ๐ธ = {๐ง โ โค โฃ โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ)} |
4 | 2, 3 | elrab2 3686 |
. . . 4
โข (๐ โ ๐ธ โ (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) |
5 | | eqeq1 2737 |
. . . . . 6
โข (๐ง = ๐ โ (๐ง = (2 ยท ๐ฅ) โ ๐ = (2 ยท ๐ฅ))) |
6 | 5 | rexbidv 3179 |
. . . . 5
โข (๐ง = ๐ โ (โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ) โ โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) |
7 | 6, 3 | elrab2 3686 |
. . . 4
โข (๐ โ ๐ธ โ (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) |
8 | | zmulcl 12608 |
. . . . . 6
โข ((๐ โ โค โง ๐ โ โค) โ (๐ ยท ๐) โ โค) |
9 | 8 | ad2ant2r 746 |
. . . . 5
โข (((๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ (๐ ยท ๐) โ โค) |
10 | | nfv 1918 |
. . . . . . . . 9
โข
โฒ๐ฅ ๐ โ โค |
11 | | nfv 1918 |
. . . . . . . . . . 11
โข
โฒ๐ฅ ๐ โ โค |
12 | | nfre1 3283 |
. . . . . . . . . . 11
โข
โฒ๐ฅโ๐ฅ โ โค ๐ = (2 ยท ๐ฅ) |
13 | 11, 12 | nfan 1903 |
. . . . . . . . . 10
โข
โฒ๐ฅ(๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) |
14 | | nfv 1918 |
. . . . . . . . . 10
โข
โฒ๐ฅโ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ) |
15 | 13, 14 | nfim 1900 |
. . . . . . . . 9
โข
โฒ๐ฅ((๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) โ โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ)) |
16 | 10, 15 | nfim 1900 |
. . . . . . . 8
โข
โฒ๐ฅ(๐ โ โค โ ((๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) โ โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ))) |
17 | | simpll 766 |
. . . . . . . . . . 11
โข (((๐ฅ โ โค โง ๐ = (2 ยท ๐ฅ)) โง ๐ โ โค) โ ๐ฅ โ โค) |
18 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) โ ๐ โ โค) |
19 | | zmulcl 12608 |
. . . . . . . . . . 11
โข ((๐ฅ โ โค โง ๐ โ โค) โ (๐ฅ ยท ๐) โ โค) |
20 | 17, 18, 19 | syl2an 597 |
. . . . . . . . . 10
โข ((((๐ฅ โ โค โง ๐ = (2 ยท ๐ฅ)) โง ๐ โ โค) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ (๐ฅ ยท ๐) โ โค) |
21 | | oveq2 7414 |
. . . . . . . . . . . 12
โข (๐ฆ = (๐ฅ ยท ๐) โ (2 ยท ๐ฆ) = (2 ยท (๐ฅ ยท ๐))) |
22 | 21 | eqeq2d 2744 |
. . . . . . . . . . 11
โข (๐ฆ = (๐ฅ ยท ๐) โ ((๐ ยท ๐) = (2 ยท ๐ฆ) โ (๐ ยท ๐) = (2 ยท (๐ฅ ยท ๐)))) |
23 | 22 | adantl 483 |
. . . . . . . . . 10
โข
(((((๐ฅ โ
โค โง ๐ = (2
ยท ๐ฅ)) โง ๐ โ โค) โง (๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ))) โง ๐ฆ = (๐ฅ ยท ๐)) โ ((๐ ยท ๐) = (2 ยท ๐ฆ) โ (๐ ยท ๐) = (2 ยท (๐ฅ ยท ๐)))) |
24 | | oveq1 7413 |
. . . . . . . . . . . 12
โข (๐ = (2 ยท ๐ฅ) โ (๐ ยท ๐) = ((2 ยท ๐ฅ) ยท ๐)) |
25 | 24 | ad3antlr 730 |
. . . . . . . . . . 11
โข ((((๐ฅ โ โค โง ๐ = (2 ยท ๐ฅ)) โง ๐ โ โค) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ (๐ ยท ๐) = ((2 ยท ๐ฅ) ยท ๐)) |
26 | | 2cnd 12287 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โค โง ๐ = (2 ยท ๐ฅ)) โง ๐ โ โค) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ 2 โ
โ) |
27 | | zcn 12560 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โค โ ๐ฅ โ
โ) |
28 | 27 | ad3antrrr 729 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โค โง ๐ = (2 ยท ๐ฅ)) โง ๐ โ โค) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ ๐ฅ โ โ) |
29 | | zcn 12560 |
. . . . . . . . . . . . . 14
โข (๐ โ โค โ ๐ โ
โ) |
30 | 29 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) โ ๐ โ โ) |
31 | 30 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ฅ โ โค โง ๐ = (2 ยท ๐ฅ)) โง ๐ โ โค) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ ๐ โ โ) |
32 | 26, 28, 31 | mulassd 11234 |
. . . . . . . . . . 11
โข ((((๐ฅ โ โค โง ๐ = (2 ยท ๐ฅ)) โง ๐ โ โค) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ ((2 ยท ๐ฅ) ยท ๐) = (2 ยท (๐ฅ ยท ๐))) |
33 | 25, 32 | eqtrd 2773 |
. . . . . . . . . 10
โข ((((๐ฅ โ โค โง ๐ = (2 ยท ๐ฅ)) โง ๐ โ โค) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ (๐ ยท ๐) = (2 ยท (๐ฅ ยท ๐))) |
34 | 20, 23, 33 | rspcedvd 3615 |
. . . . . . . . 9
โข ((((๐ฅ โ โค โง ๐ = (2 ยท ๐ฅ)) โง ๐ โ โค) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ)) |
35 | 34 | exp41 436 |
. . . . . . . 8
โข (๐ฅ โ โค โ (๐ = (2 ยท ๐ฅ) โ (๐ โ โค โ ((๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ)) โ โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ))))) |
36 | 16, 35 | rexlimi 3257 |
. . . . . . 7
โข
(โ๐ฅ โ
โค ๐ = (2 ยท
๐ฅ) โ (๐ โ โค โ ((๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) โ โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ)))) |
37 | 36 | impcom 409 |
. . . . . 6
โข ((๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) โ ((๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ)) โ โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ))) |
38 | 37 | imp 408 |
. . . . 5
โข (((๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ)) |
39 | | eqeq1 2737 |
. . . . . . . 8
โข (๐ง = (๐ ยท ๐) โ (๐ง = (2 ยท ๐ฅ) โ (๐ ยท ๐) = (2 ยท ๐ฅ))) |
40 | 39 | rexbidv 3179 |
. . . . . . 7
โข (๐ง = (๐ ยท ๐) โ (โ๐ฅ โ โค ๐ง = (2 ยท ๐ฅ) โ โ๐ฅ โ โค (๐ ยท ๐) = (2 ยท ๐ฅ))) |
41 | 40, 3 | elrab2 3686 |
. . . . . 6
โข ((๐ ยท ๐) โ ๐ธ โ ((๐ ยท ๐) โ โค โง โ๐ฅ โ โค (๐ ยท ๐) = (2 ยท ๐ฅ))) |
42 | | oveq2 7414 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (2 ยท ๐ฅ) = (2 ยท ๐ฆ)) |
43 | 42 | eqeq2d 2744 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ ((๐ ยท ๐) = (2 ยท ๐ฅ) โ (๐ ยท ๐) = (2 ยท ๐ฆ))) |
44 | 43 | cbvrexvw 3236 |
. . . . . . 7
โข
(โ๐ฅ โ
โค (๐ ยท ๐) = (2 ยท ๐ฅ) โ โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ)) |
45 | 44 | anbi2i 624 |
. . . . . 6
โข (((๐ ยท ๐) โ โค โง โ๐ฅ โ โค (๐ ยท ๐) = (2 ยท ๐ฅ)) โ ((๐ ยท ๐) โ โค โง โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ))) |
46 | 41, 45 | bitri 275 |
. . . . 5
โข ((๐ ยท ๐) โ ๐ธ โ ((๐ ยท ๐) โ โค โง โ๐ฆ โ โค (๐ ยท ๐) = (2 ยท ๐ฆ))) |
47 | 9, 38, 46 | sylanbrc 584 |
. . . 4
โข (((๐ โ โค โง
โ๐ฅ โ โค
๐ = (2 ยท ๐ฅ)) โง (๐ โ โค โง โ๐ฅ โ โค ๐ = (2 ยท ๐ฅ))) โ (๐ ยท ๐) โ ๐ธ) |
48 | 4, 7, 47 | syl2anb 599 |
. . 3
โข ((๐ โ ๐ธ โง ๐ โ ๐ธ) โ (๐ ยท ๐) โ ๐ธ) |
49 | 48 | rgen2 3198 |
. 2
โข
โ๐ โ
๐ธ โ๐ โ ๐ธ (๐ ยท ๐) โ ๐ธ |
50 | 3 | 0even 46783 |
. . 3
โข 0 โ
๐ธ |
51 | | 2zrngmmgm.1 |
. . . . 5
โข ๐ = (mulGrpโ๐
) |
52 | | 2zrngbas.r |
. . . . . 6
โข ๐
= (โfld
โพs ๐ธ) |
53 | 3, 52 | 2zrngbas 46788 |
. . . . 5
โข ๐ธ = (Baseโ๐
) |
54 | 51, 53 | mgpbas 19988 |
. . . 4
โข ๐ธ = (Baseโ๐) |
55 | 3, 52 | 2zrngmul 46797 |
. . . . 5
โข ยท
= (.rโ๐
) |
56 | 51, 55 | mgpplusg 19986 |
. . . 4
โข ยท
= (+gโ๐) |
57 | 54, 56 | ismgmn0 18560 |
. . 3
โข (0 โ
๐ธ โ (๐ โ Mgm โ โ๐ โ ๐ธ โ๐ โ ๐ธ (๐ ยท ๐) โ ๐ธ)) |
58 | 50, 57 | ax-mp 5 |
. 2
โข (๐ โ Mgm โ โ๐ โ ๐ธ โ๐ โ ๐ธ (๐ ยท ๐) โ ๐ธ) |
59 | 49, 58 | mpbir 230 |
1
โข ๐ โ Mgm |