Step |
Hyp |
Ref |
Expression |
1 |
|
invrvald.b |
โข ๐ต = ( Base โ ๐
) |
2 |
|
invrvald.t |
โข ยท = ( .r โ ๐
) |
3 |
|
invrvald.o |
โข 1 = ( 1r โ ๐
) |
4 |
|
invrvald.u |
โข ๐ = ( Unit โ ๐
) |
5 |
|
invrvald.i |
โข ๐ผ = ( invr โ ๐
) |
6 |
|
invrvald.r |
โข ( ๐ โ ๐
โ Ring ) |
7 |
|
invrvald.x |
โข ( ๐ โ ๐ โ ๐ต ) |
8 |
|
invrvald.y |
โข ( ๐ โ ๐ โ ๐ต ) |
9 |
|
invrvald.xy |
โข ( ๐ โ ( ๐ ยท ๐ ) = 1 ) |
10 |
|
invrvald.yx |
โข ( ๐ โ ( ๐ ยท ๐ ) = 1 ) |
11 |
|
eqid |
โข ( โฅr โ ๐
) = ( โฅr โ ๐
) |
12 |
1 11 2
|
dvdsrmul |
โข ( ( ๐ โ ๐ต โง ๐ โ ๐ต ) โ ๐ ( โฅr โ ๐
) ( ๐ ยท ๐ ) ) |
13 |
7 8 12
|
syl2anc |
โข ( ๐ โ ๐ ( โฅr โ ๐
) ( ๐ ยท ๐ ) ) |
14 |
13 10
|
breqtrd |
โข ( ๐ โ ๐ ( โฅr โ ๐
) 1 ) |
15 |
|
eqid |
โข ( oppr โ ๐
) = ( oppr โ ๐
) |
16 |
15 1
|
opprbas |
โข ๐ต = ( Base โ ( oppr โ ๐
) ) |
17 |
|
eqid |
โข ( โฅr โ ( oppr โ ๐
) ) = ( โฅr โ ( oppr โ ๐
) ) |
18 |
|
eqid |
โข ( .r โ ( oppr โ ๐
) ) = ( .r โ ( oppr โ ๐
) ) |
19 |
16 17 18
|
dvdsrmul |
โข ( ( ๐ โ ๐ต โง ๐ โ ๐ต ) โ ๐ ( โฅr โ ( oppr โ ๐
) ) ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) ) |
20 |
7 8 19
|
syl2anc |
โข ( ๐ โ ๐ ( โฅr โ ( oppr โ ๐
) ) ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) ) |
21 |
1 2 15 18
|
opprmul |
โข ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) = ( ๐ ยท ๐ ) |
22 |
21 9
|
eqtrid |
โข ( ๐ โ ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) = 1 ) |
23 |
20 22
|
breqtrd |
โข ( ๐ โ ๐ ( โฅr โ ( oppr โ ๐
) ) 1 ) |
24 |
4 3 11 15 17
|
isunit |
โข ( ๐ โ ๐ โ ( ๐ ( โฅr โ ๐
) 1 โง ๐ ( โฅr โ ( oppr โ ๐
) ) 1 ) ) |
25 |
14 23 24
|
sylanbrc |
โข ( ๐ โ ๐ โ ๐ ) |
26 |
|
eqid |
โข ( ( mulGrp โ ๐
) โพs ๐ ) = ( ( mulGrp โ ๐
) โพs ๐ ) |
27 |
4 26 3
|
unitgrpid |
โข ( ๐
โ Ring โ 1 = ( 0g โ ( ( mulGrp โ ๐
) โพs ๐ ) ) ) |
28 |
6 27
|
syl |
โข ( ๐ โ 1 = ( 0g โ ( ( mulGrp โ ๐
) โพs ๐ ) ) ) |
29 |
9 28
|
eqtrd |
โข ( ๐ โ ( ๐ ยท ๐ ) = ( 0g โ ( ( mulGrp โ ๐
) โพs ๐ ) ) ) |
30 |
4 26
|
unitgrp |
โข ( ๐
โ Ring โ ( ( mulGrp โ ๐
) โพs ๐ ) โ Grp ) |
31 |
6 30
|
syl |
โข ( ๐ โ ( ( mulGrp โ ๐
) โพs ๐ ) โ Grp ) |
32 |
1 11 2
|
dvdsrmul |
โข ( ( ๐ โ ๐ต โง ๐ โ ๐ต ) โ ๐ ( โฅr โ ๐
) ( ๐ ยท ๐ ) ) |
33 |
8 7 32
|
syl2anc |
โข ( ๐ โ ๐ ( โฅr โ ๐
) ( ๐ ยท ๐ ) ) |
34 |
33 9
|
breqtrd |
โข ( ๐ โ ๐ ( โฅr โ ๐
) 1 ) |
35 |
16 17 18
|
dvdsrmul |
โข ( ( ๐ โ ๐ต โง ๐ โ ๐ต ) โ ๐ ( โฅr โ ( oppr โ ๐
) ) ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) ) |
36 |
8 7 35
|
syl2anc |
โข ( ๐ โ ๐ ( โฅr โ ( oppr โ ๐
) ) ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) ) |
37 |
1 2 15 18
|
opprmul |
โข ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) = ( ๐ ยท ๐ ) |
38 |
37 10
|
eqtrid |
โข ( ๐ โ ( ๐ ( .r โ ( oppr โ ๐
) ) ๐ ) = 1 ) |
39 |
36 38
|
breqtrd |
โข ( ๐ โ ๐ ( โฅr โ ( oppr โ ๐
) ) 1 ) |
40 |
4 3 11 15 17
|
isunit |
โข ( ๐ โ ๐ โ ( ๐ ( โฅr โ ๐
) 1 โง ๐ ( โฅr โ ( oppr โ ๐
) ) 1 ) ) |
41 |
34 39 40
|
sylanbrc |
โข ( ๐ โ ๐ โ ๐ ) |
42 |
4 26
|
unitgrpbas |
โข ๐ = ( Base โ ( ( mulGrp โ ๐
) โพs ๐ ) ) |
43 |
4
|
fvexi |
โข ๐ โ V |
44 |
|
eqid |
โข ( mulGrp โ ๐
) = ( mulGrp โ ๐
) |
45 |
44 2
|
mgpplusg |
โข ยท = ( +g โ ( mulGrp โ ๐
) ) |
46 |
26 45
|
ressplusg |
โข ( ๐ โ V โ ยท = ( +g โ ( ( mulGrp โ ๐
) โพs ๐ ) ) ) |
47 |
43 46
|
ax-mp |
โข ยท = ( +g โ ( ( mulGrp โ ๐
) โพs ๐ ) ) |
48 |
|
eqid |
โข ( 0g โ ( ( mulGrp โ ๐
) โพs ๐ ) ) = ( 0g โ ( ( mulGrp โ ๐
) โพs ๐ ) ) |
49 |
4 26 5
|
invrfval |
โข ๐ผ = ( invg โ ( ( mulGrp โ ๐
) โพs ๐ ) ) |
50 |
42 47 48 49
|
grpinvid1 |
โข ( ( ( ( mulGrp โ ๐
) โพs ๐ ) โ Grp โง ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ๐ผ โ ๐ ) = ๐ โ ( ๐ ยท ๐ ) = ( 0g โ ( ( mulGrp โ ๐
) โพs ๐ ) ) ) ) |
51 |
31 25 41 50
|
syl3anc |
โข ( ๐ โ ( ( ๐ผ โ ๐ ) = ๐ โ ( ๐ ยท ๐ ) = ( 0g โ ( ( mulGrp โ ๐
) โพs ๐ ) ) ) ) |
52 |
29 51
|
mpbird |
โข ( ๐ โ ( ๐ผ โ ๐ ) = ๐ ) |
53 |
25 52
|
jca |
โข ( ๐ โ ( ๐ โ ๐ โง ( ๐ผ โ ๐ ) = ๐ ) ) |