# 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 ${⊢}{\phi }\to {K}={\mathrm{Base}}_{{R}}$
issrngd.p
issrngd.t
issrngd.c
issrngd.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
issrngd.cl
issrngd.dp
issrngd.dt
issrngd.id
Assertion issrngd ${⊢}{\phi }\to {R}\in \mathrm{*-Ring}$

### Proof

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