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 |
|
isdrngrd.k |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( x .x. I ) = .1. ) |
11 |
|
eqid |
|- ( oppR ` R ) = ( oppR ` R ) |
12 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
13 |
11 12
|
opprbas |
|- ( Base ` R ) = ( Base ` ( oppR ` R ) ) |
14 |
1 13
|
eqtrdi |
|- ( ph -> B = ( Base ` ( oppR ` R ) ) ) |
15 |
|
eqidd |
|- ( ph -> ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) ) ) |
16 |
|
eqid |
|- ( 0g ` R ) = ( 0g ` R ) |
17 |
11 16
|
oppr0 |
|- ( 0g ` R ) = ( 0g ` ( oppR ` R ) ) |
18 |
3 17
|
eqtrdi |
|- ( ph -> .0. = ( 0g ` ( oppR ` R ) ) ) |
19 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
20 |
11 19
|
oppr1 |
|- ( 1r ` R ) = ( 1r ` ( oppR ` R ) ) |
21 |
4 20
|
eqtrdi |
|- ( ph -> .1. = ( 1r ` ( oppR ` R ) ) ) |
22 |
11
|
opprring |
|- ( R e. Ring -> ( oppR ` R ) e. Ring ) |
23 |
5 22
|
syl |
|- ( ph -> ( oppR ` R ) e. Ring ) |
24 |
|
eleq1w |
|- ( y = x -> ( y e. B <-> x e. B ) ) |
25 |
|
neeq1 |
|- ( y = x -> ( y =/= .0. <-> x =/= .0. ) ) |
26 |
24 25
|
anbi12d |
|- ( y = x -> ( ( y e. B /\ y =/= .0. ) <-> ( x e. B /\ x =/= .0. ) ) ) |
27 |
26
|
3anbi2d |
|- ( y = x -> ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) <-> ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) ) ) |
28 |
|
oveq1 |
|- ( y = x -> ( y ( .r ` ( oppR ` R ) ) z ) = ( x ( .r ` ( oppR ` R ) ) z ) ) |
29 |
28
|
neeq1d |
|- ( y = x -> ( ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. <-> ( x ( .r ` ( oppR ` R ) ) z ) =/= .0. ) ) |
30 |
27 29
|
imbi12d |
|- ( y = x -> ( ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. ) <-> ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( x ( .r ` ( oppR ` R ) ) z ) =/= .0. ) ) ) |
31 |
|
eleq1w |
|- ( x = z -> ( x e. B <-> z e. B ) ) |
32 |
|
neeq1 |
|- ( x = z -> ( x =/= .0. <-> z =/= .0. ) ) |
33 |
31 32
|
anbi12d |
|- ( x = z -> ( ( x e. B /\ x =/= .0. ) <-> ( z e. B /\ z =/= .0. ) ) ) |
34 |
33
|
3anbi3d |
|- ( x = z -> ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( x e. B /\ x =/= .0. ) ) <-> ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) ) ) |
35 |
|
oveq2 |
|- ( x = z -> ( y ( .r ` ( oppR ` R ) ) x ) = ( y ( .r ` ( oppR ` R ) ) z ) ) |
36 |
35
|
neeq1d |
|- ( x = z -> ( ( y ( .r ` ( oppR ` R ) ) x ) =/= .0. <-> ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. ) ) |
37 |
34 36
|
imbi12d |
|- ( x = z -> ( ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( x e. B /\ x =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) x ) =/= .0. ) <-> ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. ) ) ) |
38 |
2
|
3ad2ant1 |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> .x. = ( .r ` R ) ) |
39 |
38
|
oveqd |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) = ( x ( .r ` R ) y ) ) |
40 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
41 |
|
eqid |
|- ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) ) |
42 |
12 40 11 41
|
opprmul |
|- ( y ( .r ` ( oppR ` R ) ) x ) = ( x ( .r ` R ) y ) |
43 |
39 42
|
eqtr4di |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) = ( y ( .r ` ( oppR ` R ) ) x ) ) |
44 |
43 6
|
eqnetrrd |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) x ) =/= .0. ) |
45 |
44
|
3com23 |
|- ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( x e. B /\ x =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) x ) =/= .0. ) |
46 |
37 45
|
chvarvv |
|- ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` ( oppR ` R ) ) z ) =/= .0. ) |
47 |
30 46
|
chvarvv |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( x ( .r ` ( oppR ` R ) ) z ) =/= .0. ) |
48 |
12 40 11 41
|
opprmul |
|- ( I ( .r ` ( oppR ` R ) ) x ) = ( x ( .r ` R ) I ) |
49 |
2
|
adantr |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> .x. = ( .r ` R ) ) |
50 |
49
|
oveqd |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( x .x. I ) = ( x ( .r ` R ) I ) ) |
51 |
50 10
|
eqtr3d |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( x ( .r ` R ) I ) = .1. ) |
52 |
48 51
|
eqtrid |
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( I ( .r ` ( oppR ` R ) ) x ) = .1. ) |
53 |
14 15 18 21 23 47 7 8 9 52
|
isdrngd |
|- ( ph -> ( oppR ` R ) e. DivRing ) |
54 |
11
|
opprdrng |
|- ( R e. DivRing <-> ( oppR ` R ) e. DivRing ) |
55 |
53 54
|
sylibr |
|- ( ph -> R e. DivRing ) |