Metamath Proof Explorer

Theorem issrngd

Description: Properties that determine a star ring. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses issrngd.k 
|- ( ph -> K = ( Base ` R ) )
issrngd.p 
|- ( ph -> .+ = ( +g ` R ) )
issrngd.t 
|- ( ph -> .x. = ( .r ` R ) )
issrngd.c 
|- ( ph -> .* = ( *r ` R ) )
issrngd.r 
|- ( ph -> R e. Ring )
issrngd.cl 
|- ( ( ph /\ x e. K ) -> ( .* ` x ) e. K )
issrngd.dp 
|- ( ( ph /\ x e. K /\ y e. K ) -> ( .* ` ( x .+ y ) ) = ( ( .* ` x ) .+ ( .* ` y ) ) )
issrngd.dt 
|- ( ( ph /\ x e. K /\ y e. K ) -> ( .* ` ( x .x. y ) ) = ( ( .* ` y ) .x. ( .* ` x ) ) )
issrngd.id 
|- ( ( ph /\ x e. K ) -> ( .* ` ( .* ` x ) ) = x )
Assertion issrngd 
|- ( ph -> R e. *Ring )

Proof

Step Hyp Ref Expression
1 issrngd.k 
 |-  ( ph -> K = ( Base ` R ) )
2 issrngd.p 
 |-  ( ph -> .+ = ( +g ` R ) )
3 issrngd.t 
 |-  ( ph -> .x. = ( .r ` R ) )
4 issrngd.c 
 |-  ( ph -> .* = ( *r ` R ) )
5 issrngd.r 
 |-  ( ph -> R e. Ring )
6 issrngd.cl 
 |-  ( ( ph /\ x e. K ) -> ( .* ` x ) e. K )
7 issrngd.dp 
 |-  ( ( ph /\ x e. K /\ y e. K ) -> ( .* ` ( x .+ y ) ) = ( ( .* ` x ) .+ ( .* ` y ) ) )
8 issrngd.dt 
 |-  ( ( ph /\ x e. K /\ y e. K ) -> ( .* ` ( x .x. y ) ) = ( ( .* ` y ) .x. ( .* ` x ) ) )
9 issrngd.id 
 |-  ( ( ph /\ x e. K ) -> ( .* ` ( .* ` x ) ) = x )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
12 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
13 12 11 oppr1 
 |-  ( 1r ` R ) = ( 1r ` ( oppR ` R ) )
14 eqid 
 |-  ( .r ` R ) = ( .r ` R )
15 eqid 
 |-  ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) )
16 12 opprring 
 |-  ( R e. Ring -> ( oppR ` R ) e. Ring )
17 5 16 syl 
 |-  ( ph -> ( oppR ` R ) e. Ring )
18 id 
 |-  ( x = ( 1r ` R ) -> x = ( 1r ` R ) )
19 fveq2 
 |-  ( x = ( 1r ` R ) -> ( ( *r ` R ) ` x ) = ( ( *r ` R ) ` ( 1r ` R ) ) )
20 19 fveq2d 
 |-  ( x = ( 1r ` R ) -> ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) = ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) )
21 18 20 eqeq12d 
 |-  ( x = ( 1r ` R ) -> ( x = ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) <-> ( 1r ` R ) = ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) ) )
22 9 ex 
 |-  ( ph -> ( x e. K -> ( .* ` ( .* ` x ) ) = x ) )
23 1 eleq2d 
 |-  ( ph -> ( x e. K <-> x e. ( Base ` R ) ) )
24 4 fveq1d 
 |-  ( ph -> ( .* ` x ) = ( ( *r ` R ) ` x ) )
25 4 24 fveq12d 
 |-  ( ph -> ( .* ` ( .* ` x ) ) = ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) )
26 25 eqeq1d 
 |-  ( ph -> ( ( .* ` ( .* ` x ) ) = x <-> ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) = x ) )
27 22 23 26 3imtr3d 
 |-  ( ph -> ( x e. ( Base ` R ) -> ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) = x ) )
28 27 imp 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) = x )
29 28 eqcomd 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> x = ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) )
30 29 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` R ) x = ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) )
31 10 11 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
32 5 31 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
33 21 30 32 rspcdva 
 |-  ( ph -> ( 1r ` R ) = ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) )
34 33 oveq1d 
 |-  ( ph -> ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) = ( ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) )
35 19 eleq1d 
 |-  ( x = ( 1r ` R ) -> ( ( ( *r ` R ) ` x ) e. ( Base ` R ) <-> ( ( *r ` R ) ` ( 1r ` R ) ) e. ( Base ` R ) ) )
36 6 ex 
 |-  ( ph -> ( x e. K -> ( .* ` x ) e. K ) )
37 24 1 eleq12d 
 |-  ( ph -> ( ( .* ` x ) e. K <-> ( ( *r ` R ) ` x ) e. ( Base ` R ) ) )
38 36 23 37 3imtr3d 
 |-  ( ph -> ( x e. ( Base ` R ) -> ( ( *r ` R ) ` x ) e. ( Base ` R ) ) )
39 38 ralrimiv 
 |-  ( ph -> A. x e. ( Base ` R ) ( ( *r ` R ) ` x ) e. ( Base ` R ) )
40 35 39 32 rspcdva 
 |-  ( ph -> ( ( *r ` R ) ` ( 1r ` R ) ) e. ( Base ` R ) )
41 8 3expib 
 |-  ( ph -> ( ( x e. K /\ y e. K ) -> ( .* ` ( x .x. y ) ) = ( ( .* ` y ) .x. ( .* ` x ) ) ) )
42 1 eleq2d 
 |-  ( ph -> ( y e. K <-> y e. ( Base ` R ) ) )
43 23 42 anbi12d 
 |-  ( ph -> ( ( x e. K /\ y e. K ) <-> ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) )
44 3 oveqd 
 |-  ( ph -> ( x .x. y ) = ( x ( .r ` R ) y ) )
45 4 44 fveq12d 
 |-  ( ph -> ( .* ` ( x .x. y ) ) = ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) )
46 4 fveq1d 
 |-  ( ph -> ( .* ` y ) = ( ( *r ` R ) ` y ) )
47 3 46 24 oveq123d 
 |-  ( ph -> ( ( .* ` y ) .x. ( .* ` x ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` x ) ) )
48 45 47 eqeq12d 
 |-  ( ph -> ( ( .* ` ( x .x. y ) ) = ( ( .* ` y ) .x. ( .* ` x ) ) <-> ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` x ) ) ) )
49 41 43 48 3imtr3d 
 |-  ( ph -> ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` x ) ) ) )
50 49 ralrimivv 
 |-  ( ph -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` x ) ) )
51 fvoveq1 
 |-  ( x = ( 1r ` R ) -> ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) = ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) y ) ) )
52 19 oveq2d 
 |-  ( x = ( 1r ` R ) -> ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` x ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) )
53 51 52 eqeq12d 
 |-  ( x = ( 1r ` R ) -> ( ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` x ) ) <-> ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) y ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) ) )
54 oveq2 
 |-  ( y = ( ( *r ` R ) ` ( 1r ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) y ) = ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) )
55 54 fveq2d 
 |-  ( y = ( ( *r ` R ) ` ( 1r ` R ) ) -> ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) y ) ) = ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) ) )
56 fveq2 
 |-  ( y = ( ( *r ` R ) ` ( 1r ` R ) ) -> ( ( *r ` R ) ` y ) = ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) )
57 56 oveq1d 
 |-  ( y = ( ( *r ` R ) ` ( 1r ` R ) ) -> ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) = ( ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) )
58 55 57 eqeq12d 
 |-  ( y = ( ( *r ` R ) ` ( 1r ` R ) ) -> ( ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) y ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) <-> ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) ) = ( ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) ) )
59 53 58 rspc2va 
 |-  ( ( ( ( 1r ` R ) e. ( Base ` R ) /\ ( ( *r ` R ) ` ( 1r ` R ) ) e. ( Base ` R ) ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` x ) ) ) -> ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) ) = ( ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) )
60 32 40 50 59 syl21anc 
 |-  ( ph -> ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) ) = ( ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) )
61 34 60 eqtr4d 
 |-  ( ph -> ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) = ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) ) )
62 10 14 11 ringlidm 
 |-  ( ( R e. Ring /\ ( ( *r ` R ) ` ( 1r ` R ) ) e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) = ( ( *r ` R ) ` ( 1r ` R ) ) )
63 5 40 62 syl2anc 
 |-  ( ph -> ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) = ( ( *r ` R ) ` ( 1r ` R ) ) )
64 63 fveq2d 
 |-  ( ph -> ( ( *r ` R ) ` ( ( 1r ` R ) ( .r ` R ) ( ( *r ` R ) ` ( 1r ` R ) ) ) ) = ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) )
65 61 63 64 3eqtr3d 
 |-  ( ph -> ( ( *r ` R ) ` ( 1r ` R ) ) = ( ( *r ` R ) ` ( ( *r ` R ) ` ( 1r ` R ) ) ) )
66 eqid 
 |-  ( *r ` R ) = ( *r ` R )
67 eqid 
 |-  ( *rf ` R ) = ( *rf ` R )
68 10 66 67 stafval 
 |-  ( ( 1r ` R ) e. ( Base ` R ) -> ( ( *rf ` R ) ` ( 1r ` R ) ) = ( ( *r ` R ) ` ( 1r ` R ) ) )
69 32 68 syl 
 |-  ( ph -> ( ( *rf ` R ) ` ( 1r ` R ) ) = ( ( *r ` R ) ` ( 1r ` R ) ) )
70 65 69 33 3eqtr4d 
 |-  ( ph -> ( ( *rf ` R ) ` ( 1r ` R ) ) = ( 1r ` R ) )
71 49 imp 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` x ) ) )
72 10 14 12 15 opprmul 
 |-  ( ( ( *r ` R ) ` x ) ( .r ` ( oppR ` R ) ) ( ( *r ` R ) ` y ) ) = ( ( ( *r ` R ) ` y ) ( .r ` R ) ( ( *r ` R ) ` x ) )
73 71 72 eqtr4di 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) = ( ( ( *r ` R ) ` x ) ( .r ` ( oppR ` R ) ) ( ( *r ` R ) ` y ) ) )
74 10 14 ringcl 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
75 74 3expb 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
76 5 75 sylan 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( .r ` R ) y ) e. ( Base ` R ) )
77 10 66 67 stafval 
 |-  ( ( x ( .r ` R ) y ) e. ( Base ` R ) -> ( ( *rf ` R ) ` ( x ( .r ` R ) y ) ) = ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) )
78 76 77 syl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( *rf ` R ) ` ( x ( .r ` R ) y ) ) = ( ( *r ` R ) ` ( x ( .r ` R ) y ) ) )
79 10 66 67 stafval 
 |-  ( x e. ( Base ` R ) -> ( ( *rf ` R ) ` x ) = ( ( *r ` R ) ` x ) )
80 10 66 67 stafval 
 |-  ( y e. ( Base ` R ) -> ( ( *rf ` R ) ` y ) = ( ( *r ` R ) ` y ) )
81 79 80 oveqan12d 
 |-  ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( ( *rf ` R ) ` x ) ( .r ` ( oppR ` R ) ) ( ( *rf ` R ) ` y ) ) = ( ( ( *r ` R ) ` x ) ( .r ` ( oppR ` R ) ) ( ( *r ` R ) ` y ) ) )
82 81 adantl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( ( *rf ` R ) ` x ) ( .r ` ( oppR ` R ) ) ( ( *rf ` R ) ` y ) ) = ( ( ( *r ` R ) ` x ) ( .r ` ( oppR ` R ) ) ( ( *r ` R ) ` y ) ) )
83 73 78 82 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( *rf ` R ) ` ( x ( .r ` R ) y ) ) = ( ( ( *rf ` R ) ` x ) ( .r ` ( oppR ` R ) ) ( ( *rf ` R ) ` y ) ) )
84 12 10 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` R ) )
85 eqid 
 |-  ( +g ` R ) = ( +g ` R )
86 12 85 oppradd 
 |-  ( +g ` R ) = ( +g ` ( oppR ` R ) )
87 38 imp 
 |-  ( ( ph /\ x e. ( Base ` R ) ) -> ( ( *r ` R ) ` x ) e. ( Base ` R ) )
88 10 66 67 staffval 
 |-  ( *rf ` R ) = ( x e. ( Base ` R ) |-> ( ( *r ` R ) ` x ) )
89 87 88 fmptd 
 |-  ( ph -> ( *rf ` R ) : ( Base ` R ) --> ( Base ` R ) )
90 7 3expib 
 |-  ( ph -> ( ( x e. K /\ y e. K ) -> ( .* ` ( x .+ y ) ) = ( ( .* ` x ) .+ ( .* ` y ) ) ) )
91 2 oveqd 
 |-  ( ph -> ( x .+ y ) = ( x ( +g ` R ) y ) )
92 4 91 fveq12d 
 |-  ( ph -> ( .* ` ( x .+ y ) ) = ( ( *r ` R ) ` ( x ( +g ` R ) y ) ) )
93 2 24 46 oveq123d 
 |-  ( ph -> ( ( .* ` x ) .+ ( .* ` y ) ) = ( ( ( *r ` R ) ` x ) ( +g ` R ) ( ( *r ` R ) ` y ) ) )
94 92 93 eqeq12d 
 |-  ( ph -> ( ( .* ` ( x .+ y ) ) = ( ( .* ` x ) .+ ( .* ` y ) ) <-> ( ( *r ` R ) ` ( x ( +g ` R ) y ) ) = ( ( ( *r ` R ) ` x ) ( +g ` R ) ( ( *r ` R ) ` y ) ) ) )
95 90 43 94 3imtr3d 
 |-  ( ph -> ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( *r ` R ) ` ( x ( +g ` R ) y ) ) = ( ( ( *r ` R ) ` x ) ( +g ` R ) ( ( *r ` R ) ` y ) ) ) )
96 95 imp 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( *r ` R ) ` ( x ( +g ` R ) y ) ) = ( ( ( *r ` R ) ` x ) ( +g ` R ) ( ( *r ` R ) ` y ) ) )
97 10 85 ringacl 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
98 97 3expb 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
99 5 98 sylan 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) e. ( Base ` R ) )
100 10 66 67 stafval 
 |-  ( ( x ( +g ` R ) y ) e. ( Base ` R ) -> ( ( *rf ` R ) ` ( x ( +g ` R ) y ) ) = ( ( *r ` R ) ` ( x ( +g ` R ) y ) ) )
101 99 100 syl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( *rf ` R ) ` ( x ( +g ` R ) y ) ) = ( ( *r ` R ) ` ( x ( +g ` R ) y ) ) )
102 79 80 oveqan12d 
 |-  ( ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( ( ( *rf ` R ) ` x ) ( +g ` R ) ( ( *rf ` R ) ` y ) ) = ( ( ( *r ` R ) ` x ) ( +g ` R ) ( ( *r ` R ) ` y ) ) )
103 102 adantl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( ( *rf ` R ) ` x ) ( +g ` R ) ( ( *rf ` R ) ` y ) ) = ( ( ( *r ` R ) ` x ) ( +g ` R ) ( ( *r ` R ) ` y ) ) )
104 96 101 103 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( ( *rf ` R ) ` ( x ( +g ` R ) y ) ) = ( ( ( *rf ` R ) ` x ) ( +g ` R ) ( ( *rf ` R ) ` y ) ) )
105 10 11 13 14 15 5 17 70 83 84 85 86 89 104 isrhmd 
 |-  ( ph -> ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) )
106 10 66 67 staffval 
 |-  ( *rf ` R ) = ( y e. ( Base ` R ) |-> ( ( *r ` R ) ` y ) )
107 106 fmpt 
 |-  ( A. y e. ( Base ` R ) ( ( *r ` R ) ` y ) e. ( Base ` R ) <-> ( *rf ` R ) : ( Base ` R ) --> ( Base ` R ) )
108 89 107 sylibr 
 |-  ( ph -> A. y e. ( Base ` R ) ( ( *r ` R ) ` y ) e. ( Base ` R ) )
109 108 r19.21bi 
 |-  ( ( ph /\ y e. ( Base ` R ) ) -> ( ( *r ` R ) ` y ) e. ( Base ` R ) )
110 id 
 |-  ( x = y -> x = y )
111 fveq2 
 |-  ( x = y -> ( ( *r ` R ) ` x ) = ( ( *r ` R ) ` y ) )
112 111 fveq2d 
 |-  ( x = y -> ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) = ( ( *r ` R ) ` ( ( *r ` R ) ` y ) ) )
113 110 112 eqeq12d 
 |-  ( x = y -> ( x = ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) <-> y = ( ( *r ` R ) ` ( ( *r ` R ) ` y ) ) ) )
114 113 rspccva 
 |-  ( ( A. x e. ( Base ` R ) x = ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) /\ y e. ( Base ` R ) ) -> y = ( ( *r ` R ) ` ( ( *r ` R ) ` y ) ) )
115 30 114 sylan 
 |-  ( ( ph /\ y e. ( Base ` R ) ) -> y = ( ( *r ` R ) ` ( ( *r ` R ) ` y ) ) )
116 115 adantrl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> y = ( ( *r ` R ) ` ( ( *r ` R ) ` y ) ) )
117 fveq2 
 |-  ( x = ( ( *r ` R ) ` y ) -> ( ( *r ` R ) ` x ) = ( ( *r ` R ) ` ( ( *r ` R ) ` y ) ) )
118 117 eqeq2d 
 |-  ( x = ( ( *r ` R ) ` y ) -> ( y = ( ( *r ` R ) ` x ) <-> y = ( ( *r ` R ) ` ( ( *r ` R ) ` y ) ) ) )
119 116 118 syl5ibrcom 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x = ( ( *r ` R ) ` y ) -> y = ( ( *r ` R ) ` x ) ) )
120 29 adantrr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> x = ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) )
121 fveq2 
 |-  ( y = ( ( *r ` R ) ` x ) -> ( ( *r ` R ) ` y ) = ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) )
122 121 eqeq2d 
 |-  ( y = ( ( *r ` R ) ` x ) -> ( x = ( ( *r ` R ) ` y ) <-> x = ( ( *r ` R ) ` ( ( *r ` R ) ` x ) ) ) )
123 120 122 syl5ibrcom 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( y = ( ( *r ` R ) ` x ) -> x = ( ( *r ` R ) ` y ) ) )
124 119 123 impbid 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x = ( ( *r ` R ) ` y ) <-> y = ( ( *r ` R ) ` x ) ) )
125 88 87 109 124 f1ocnv2d 
 |-  ( ph -> ( ( *rf ` R ) : ( Base ` R ) -1-1-onto-> ( Base ` R ) /\ `' ( *rf ` R ) = ( y e. ( Base ` R ) |-> ( ( *r ` R ) ` y ) ) ) )
126 125 simprd 
 |-  ( ph -> `' ( *rf ` R ) = ( y e. ( Base ` R ) |-> ( ( *r ` R ) ` y ) ) )
127 106 126 eqtr4id 
 |-  ( ph -> ( *rf ` R ) = `' ( *rf ` R ) )
128 12 67 issrng 
 |-  ( R e. *Ring <-> ( ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) /\ ( *rf ` R ) = `' ( *rf ` R ) ) )
129 105 127 128 sylanbrc 
 |-  ( ph -> R e. *Ring )