This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isdrngrdOLD

Description: Obsolete version of isdrngrd as of 19-Feb-2025. (Contributed by NM, 10-Aug-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses isdrngdOLD.b 
|- ( ph -> B = ( Base ` R ) )
isdrngdOLD.t 
|- ( ph -> .x. = ( .r ` R ) )
isdrngdOLD.z 
|- ( ph -> .0. = ( 0g ` R ) )
isdrngdOLD.u 
|- ( ph -> .1. = ( 1r ` R ) )
isdrngdOLD.r 
|- ( ph -> R e. Ring )
isdrngdOLD.n 
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) =/= .0. )
isdrngdOLD.o 
|- ( ph -> .1. =/= .0. )
isdrngdOLD.i 
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I e. B )
isdrngdOLD.j 
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I =/= .0. )
isdrngrdOLD.k 
|- ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> ( x .x. I ) = .1. )
Assertion isdrngrdOLD 
|- ( ph -> R e. DivRing )

Proof

Step Hyp Ref Expression
1 isdrngdOLD.b 
 |-  ( ph -> B = ( Base ` R ) )
2 isdrngdOLD.t 
 |-  ( ph -> .x. = ( .r ` R ) )
3 isdrngdOLD.z 
 |-  ( ph -> .0. = ( 0g ` R ) )
4 isdrngdOLD.u 
 |-  ( ph -> .1. = ( 1r ` R ) )
5 isdrngdOLD.r 
 |-  ( ph -> R e. Ring )
6 isdrngdOLD.n 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x .x. y ) =/= .0. )
7 isdrngdOLD.o 
 |-  ( ph -> .1. =/= .0. )
8 isdrngdOLD.i 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I e. B )
9 isdrngdOLD.j 
 |-  ( ( ph /\ ( x e. B /\ x =/= .0. ) ) -> I =/= .0. )
10 isdrngrdOLD.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 isdrngdOLD 
 |-  ( ph -> ( oppR ` R ) e. DivRing )
54 11 opprdrng 
 |-  ( R e. DivRing <-> ( oppR ` R ) e. DivRing )
55 53 54 sylibr 
 |-  ( ph -> R e. DivRing )