Step |
Hyp |
Ref |
Expression |
1 |
|
isdrngd.b |
|- ( ph -> B = ( Base ` R ) ) |
2 |
|
isdrngd.t |
|- ( ph -> .x. = ( .r ` R ) ) |
3 |
|
isdrngd.z |
|- ( ph -> .0. = ( 0g ` R ) ) |
4 |
|
isdrngd.u |
|- ( ph -> .1. = ( 1r ` R ) ) |
5 |
|
isdrngd.r |
|- ( ph -> R e. Ring ) |
6 |
|
isdrngd.n |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) =/= .0. ) |
7 |
|
isdrngd.o |
|- ( ph -> .1. =/= .0. ) |
8 |
|
isdrngd.i |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I e. B ) |
9 |
|
isdrngd.j |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I =/= .0. ) |
10 |
|
isdrngd.k |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( I .x. x ) = .1. ) |
11 |
|
difss |
|- ( B \ { .0. } ) C_ B |
12 |
11 1
|
sseqtrid |
|- ( ph -> ( B \ { .0. } ) C_ ( Base ` R ) ) |
13 |
|
eqid |
|- ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) |
14 |
|
eqid |
|- ( mulGrp ` R ) = ( mulGrp ` R ) |
15 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
16 |
14 15
|
mgpbas |
|- ( Base ` R ) = ( Base ` ( mulGrp ` R ) ) |
17 |
13 16
|
ressbas2 |
|- ( ( B \ { .0. } ) C_ ( Base ` R ) -> ( B \ { .0. } ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) |
18 |
12 17
|
syl |
|- ( ph -> ( B \ { .0. } ) = ( Base ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) |
19 |
|
fvex |
|- ( Base ` R ) e. _V |
20 |
1 19
|
eqeltrdi |
|- ( ph -> B e. _V ) |
21 |
|
difexg |
|- ( B e. _V -> ( B \ { .0. } ) e. _V ) |
22 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
23 |
14 22
|
mgpplusg |
|- ( .r ` R ) = ( +g ` ( mulGrp ` R ) ) |
24 |
13 23
|
ressplusg |
|- ( ( B \ { .0. } ) e. _V -> ( .r ` R ) = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) |
25 |
20 21 24
|
3syl |
|- ( ph -> ( .r ` R ) = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) |
26 |
2 25
|
eqtrd |
|- ( ph -> .x. = ( +g ` ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) ) ) |
27 |
|
eldifsn |
|- ( x e. ( B \ { .0. } ) <-> ( x e. B /\ x =/= .0. ) ) |
28 |
|
eldifsn |
|- ( y e. ( B \ { .0. } ) <-> ( y e. B /\ y =/= .0. ) ) |
29 |
15 22
|
ringcl |
|- ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) ) |
30 |
5 29
|
syl3an1 |
|- ( ( ph /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) ) |
31 |
30
|
3expib |
|- ( ph -> ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) ) ) |
32 |
1
|
eleq2d |
|- ( ph -> ( x e. B <-> x e. ( Base ` R ) ) ) |
33 |
1
|
eleq2d |
|- ( ph -> ( y e. B <-> y e. ( Base ` R ) ) ) |
34 |
32 33
|
anbi12d |
|- ( ph -> ( ( x e. B /\ y e. B ) <-> ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) ) |
35 |
2
|
oveqd |
|- ( ph -> ( x .x. y ) = ( x ( .r ` R ) y ) ) |
36 |
35 1
|
eleq12d |
|- ( ph -> ( ( x .x. y ) e. B <-> ( x ( .r ` R ) y ) e. ( Base ` R ) ) ) |
37 |
31 34 36
|
3imtr4d |
|- ( ph -> ( ( x e. B /\ y e. B ) -> ( x .x. y ) e. B ) ) |
38 |
37
|
3impib |
|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .x. y ) e. B ) |
39 |
38
|
3adant2r |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ y e. B ) -> ( x .x. y ) e. B ) |
40 |
39
|
3adant3r |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) e. B ) |
41 |
|
eldifsn |
|- ( ( x .x. y ) e. ( B \ { .0. } ) <-> ( ( x .x. y ) e. B /\ ( x .x. y ) =/= .0. ) ) |
42 |
40 6 41
|
sylanbrc |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) e. ( B \ { .0. } ) ) |
43 |
28 42
|
syl3an3b |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ y e. ( B \ { .0. } ) ) -> ( x .x. y ) e. ( B \ { .0. } ) ) |
44 |
27 43
|
syl3an2b |
|- ( ( ph /\ x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) -> ( x .x. y ) e. ( B \ { .0. } ) ) |
45 |
15 22
|
ringass |
|- ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) ) |
46 |
45
|
ex |
|- ( R e. Ring -> ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) ) ) |
47 |
5 46
|
syl |
|- ( ph -> ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) -> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) ) ) |
48 |
1
|
eleq2d |
|- ( ph -> ( z e. B <-> z e. ( Base ` R ) ) ) |
49 |
32 33 48
|
3anbi123d |
|- ( ph -> ( ( x e. B /\ y e. B /\ z e. B ) <-> ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) ) |
50 |
|
eqidd |
|- ( ph -> z = z ) |
51 |
2 35 50
|
oveq123d |
|- ( ph -> ( ( x .x. y ) .x. z ) = ( ( x ( .r ` R ) y ) ( .r ` R ) z ) ) |
52 |
|
eqidd |
|- ( ph -> x = x ) |
53 |
2
|
oveqd |
|- ( ph -> ( y .x. z ) = ( y ( .r ` R ) z ) ) |
54 |
2 52 53
|
oveq123d |
|- ( ph -> ( x .x. ( y .x. z ) ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) ) |
55 |
51 54
|
eqeq12d |
|- ( ph -> ( ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) <-> ( ( x ( .r ` R ) y ) ( .r ` R ) z ) = ( x ( .r ` R ) ( y ( .r ` R ) z ) ) ) ) |
56 |
47 49 55
|
3imtr4d |
|- ( ph -> ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) ) |
57 |
|
eldifi |
|- ( x e. ( B \ { .0. } ) -> x e. B ) |
58 |
|
eldifi |
|- ( y e. ( B \ { .0. } ) -> y e. B ) |
59 |
|
eldifi |
|- ( z e. ( B \ { .0. } ) -> z e. B ) |
60 |
57 58 59
|
3anim123i |
|- ( ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) /\ z e. ( B \ { .0. } ) ) -> ( x e. B /\ y e. B /\ z e. B ) ) |
61 |
56 60
|
impel |
|- ( ( ph /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) /\ z e. ( B \ { .0. } ) ) ) -> ( ( x .x. y ) .x. z ) = ( x .x. ( y .x. z ) ) ) |
62 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
63 |
15 62
|
ringidcl |
|- ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) ) |
64 |
5 63
|
syl |
|- ( ph -> ( 1r ` R ) e. ( Base ` R ) ) |
65 |
64 4 1
|
3eltr4d |
|- ( ph -> .1. e. B ) |
66 |
|
eldifsn |
|- ( .1. e. ( B \ { .0. } ) <-> ( .1. e. B /\ .1. =/= .0. ) ) |
67 |
65 7 66
|
sylanbrc |
|- ( ph -> .1. e. ( B \ { .0. } ) ) |
68 |
15 22 62
|
ringlidm |
|- ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x ) |
69 |
68
|
ex |
|- ( R e. Ring -> ( x e. ( Base ` R ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x ) ) |
70 |
5 69
|
syl |
|- ( ph -> ( x e. ( Base ` R ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x ) ) |
71 |
2 4 52
|
oveq123d |
|- ( ph -> ( .1. .x. x ) = ( ( 1r ` R ) ( .r ` R ) x ) ) |
72 |
71
|
eqeq1d |
|- ( ph -> ( ( .1. .x. x ) = x <-> ( ( 1r ` R ) ( .r ` R ) x ) = x ) ) |
73 |
70 32 72
|
3imtr4d |
|- ( ph -> ( x e. B -> ( .1. .x. x ) = x ) ) |
74 |
73
|
imp |
|- ( ( ph /\ x e. B ) -> ( .1. .x. x ) = x ) |
75 |
74
|
adantrr |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( .1. .x. x ) = x ) |
76 |
27 75
|
sylan2b |
|- ( ( ph /\ x e. ( B \ { .0. } ) ) -> ( .1. .x. x ) = x ) |
77 |
|
eldifsn |
|- ( I e. ( B \ { .0. } ) <-> ( I e. B /\ I =/= .0. ) ) |
78 |
8 9 77
|
sylanbrc |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I e. ( B \ { .0. } ) ) |
79 |
27 78
|
sylan2b |
|- ( ( ph /\ x e. ( B \ { .0. } ) ) -> I e. ( B \ { .0. } ) ) |
80 |
27 10
|
sylan2b |
|- ( ( ph /\ x e. ( B \ { .0. } ) ) -> ( I .x. x ) = .1. ) |
81 |
18 26 44 61 67 76 79 80
|
isgrpd |
|- ( ph -> ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) |
82 |
3
|
sneqd |
|- ( ph -> { .0. } = { ( 0g ` R ) } ) |
83 |
1 82
|
difeq12d |
|- ( ph -> ( B \ { .0. } ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) ) |
84 |
83
|
oveq2d |
|- ( ph -> ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) = ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) ) |
85 |
84
|
eleq1d |
|- ( ph -> ( ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp <-> ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) e. Grp ) ) |
86 |
85
|
anbi2d |
|- ( ph -> ( ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( B \ { .0. } ) ) e. Grp ) <-> ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) e. Grp ) ) ) |
87 |
5 81 86
|
mpbi2and |
|- ( ph -> ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) e. Grp ) ) |
88 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
89 |
|
eqid |
|- ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) = ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) |
90 |
15 88 89
|
isdrng2 |
|- ( R e. DivRing <-> ( R e. Ring /\ ( ( mulGrp ` R ) |`s ( ( Base ` R ) \ { ( 0g ` R ) } ) ) e. Grp ) ) |
91 |
87 90
|
sylibr |
|- ( ph -> R e. DivRing ) |