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	$$⊢\phi \to \underset{\dot{}}{+}={+}_R$$
	issrngd.t	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
	issrngd.c	$$⊢\phi \to \underset{\dot{}}{\ast }={\mathrm{*}}_R$$
	issrngd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	issrngd.cl	$$⊢\left(\phi \wedge x\in K\right)\to \underset{\dot{}}{\ast }\left(x\right)\in K$$
	issrngd.dp	$$⊢\left(\phi \wedge x\in K\wedge y\in K\right)\to \underset{\dot{}}{\ast }\left(x\underset{\dot{}}{+}y\right)=\underset{\dot{}}{\ast }\left(x\right)\underset{\dot{}}{+}\underset{\dot{}}{\ast }\left(y\right)$$
	issrngd.dt	$$⊢\left(\phi \wedge x\in K\wedge y\in K\right)\to \underset{\dot{}}{\ast }\left(x\underset{\dot{}}{·}y\right)=\underset{\dot{}}{\ast }\left(y\right)\underset{\dot{}}{·}\underset{\dot{}}{\ast }\left(x\right)$$
	issrngd.id	$$⊢\left(\phi \wedge x\in K\right)\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(x\right)\right)=x$$
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	$$⊢\phi \to \underset{\dot{}}{+}={+}_R$$
3		issrngd.t	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
4		issrngd.c	$$⊢\phi \to \underset{\dot{}}{\ast }={\mathrm{*}}_R$$
5		issrngd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		issrngd.cl	$$⊢\left(\phi \wedge x\in K\right)\to \underset{\dot{}}{\ast }\left(x\right)\in K$$
7		issrngd.dp	$$⊢\left(\phi \wedge x\in K\wedge y\in K\right)\to \underset{\dot{}}{\ast }\left(x\underset{\dot{}}{+}y\right)=\underset{\dot{}}{\ast }\left(x\right)\underset{\dot{}}{+}\underset{\dot{}}{\ast }\left(y\right)$$
8		issrngd.dt	$$⊢\left(\phi \wedge x\in K\wedge y\in K\right)\to \underset{\dot{}}{\ast }\left(x\underset{\dot{}}{·}y\right)=\underset{\dot{}}{\ast }\left(y\right)\underset{\dot{}}{·}\underset{\dot{}}{\ast }\left(x\right)$$
9		issrngd.id	$$⊢\left(\phi \wedge x\in K\right)\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(x\right)\right)=x$$
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^{{\mathrm{*}}_R}={1_R}^{{\mathrm{*}}_R}$$
20	19	fveq2d	$$⊢x=1_R\to {x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
21	18 20	eqeq12d	$$⊢x=1_R\to \left(x={x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}\leftrightarrow 1_R={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}\right)$$
22	9	ex	$$⊢\phi \to \left(x\in K\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(x\right)\right)=x\right)$$
23	1	eleq2d	$$⊢\phi \to \left(x\in K\leftrightarrow x\in {\mathrm{Base}}_R\right)$$
24	4	fveq1d	$$⊢\phi \to \underset{\dot{}}{\ast }\left(x\right)=x^{{\mathrm{*}}_R}$$
25	4 24	fveq12d	$$⊢\phi \to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(x\right)\right)={x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
26	25	eqeq1d	$$⊢\phi \to \left(\underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(x\right)\right)=x\leftrightarrow {x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}=x\right)$$
27	22 23 26	3imtr3d	$$⊢\phi \to \left(x\in {\mathrm{Base}}_R\to {x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}=x\right)$$
28	27	imp	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to {x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}=x$$
29	28	eqcomd	$$⊢\left(\phi \wedge x\in {\mathrm{Base}}_R\right)\to x={x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
30	29	ralrimiva	$$⊢\phi \to \forall x\in {\mathrm{Base}}_{R}x={x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_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}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
34	33	oveq1d	$$⊢\phi \to 1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}{\cdot }_R{1_R}^{{\mathrm{*}}_R}$$
35	19	eleq1d	$$⊢x=1_R\to \left(x^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R\leftrightarrow {1_R}^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R\right)$$
36	6	ex	$$⊢\phi \to \left(x\in K\to \underset{\dot{}}{\ast }\left(x\right)\in K\right)$$
37	24 1	eleq12d	$$⊢\phi \to \left(\underset{\dot{}}{\ast }\left(x\right)\in K\leftrightarrow x^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R\right)$$
38	36 23 37	3imtr3d	$$⊢\phi \to \left(x\in {\mathrm{Base}}_R\to x^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R\right)$$
39	38	ralrimiv	$$⊢\phi \to \forall x\in {\mathrm{Base}}_R{x}^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R$$
40	35 39 32	rspcdva	$$⊢\phi \to {1_R}^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R$$
41	8	3expib	$$⊢\phi \to \left(\left(x\in K\wedge y\in K\right)\to \underset{\dot{}}{\ast }\left(x\underset{\dot{}}{·}y\right)=\underset{\dot{}}{\ast }\left(y\right)\underset{\dot{}}{·}\underset{\dot{}}{\ast }\left(x\right)\right)$$
42	1	eleq2d	$$⊢\phi \to \left(y\in K\leftrightarrow y\in {\mathrm{Base}}_R\right)$$
43	23 42	anbi12d	$$⊢\phi \to \left(\left(x\in K\wedge y\in K\right)\leftrightarrow \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)$$
44	3	oveqd	$$⊢\phi \to x\underset{\dot{}}{·}y=x{\cdot }_{R}y$$
45	4 44	fveq12d	$$⊢\phi \to \underset{\dot{}}{\ast }\left(x\underset{\dot{}}{·}y\right)={\left(x{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}$$
46	4	fveq1d	$$⊢\phi \to \underset{\dot{}}{\ast }\left(y\right)=y^{{\mathrm{*}}_R}$$
47	3 46 24	oveq123d	$$⊢\phi \to \underset{\dot{}}{\ast }\left(y\right)\underset{\dot{}}{·}\underset{\dot{}}{\ast }\left(x\right)=y^{{\mathrm{*}}_R}{\cdot }_R{x}^{{\mathrm{*}}_R}$$
48	45 47	eqeq12d	$$⊢\phi \to \left(\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{·}y\right)=\underset{\dot{}}{\ast }\left(y\right)\underset{\dot{}}{·}\underset{\dot{}}{\ast }\left(x\right)\leftrightarrow {\left(x{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{x}^{{\mathrm{*}}_R}\right)$$
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)}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{x}^{{\mathrm{*}}_R}\right)$$
50	49	ralrimivv	$$⊢\phi \to \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R{\left(x{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{x}^{{\mathrm{*}}_R}$$
51		fvoveq1	$$⊢x=1_R\to {\left(x{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}={\left(1_R{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}$$
52	19	oveq2d	$$⊢x=1_R\to y^{{\mathrm{*}}_R}{\cdot }_R{x}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{1_R}^{{\mathrm{*}}_R}$$
53	51 52	eqeq12d	$$⊢x=1_R\to \left({\left(x{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{x}^{{\mathrm{*}}_R}\leftrightarrow {\left(1_R{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{1_R}^{{\mathrm{*}}_R}\right)$$
54		oveq2	$$⊢y={1_R}^{{\mathrm{*}}_R}\to 1_R{\cdot }_{R}y=1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}$$
55	54	fveq2d	$$⊢y={1_R}^{{\mathrm{*}}_R}\to {\left(1_R{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}={\left(1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}\right)}^{{\mathrm{*}}_R}$$
56		fveq2	$$⊢y={1_R}^{{\mathrm{*}}_R}\to y^{{\mathrm{*}}_R}={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
57	56	oveq1d	$$⊢y={1_R}^{{\mathrm{*}}_R}\to y^{{\mathrm{*}}_R}{\cdot }_R{1_R}^{{\mathrm{*}}_R}={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}{\cdot }_R{1_R}^{{\mathrm{*}}_R}$$
58	55 57	eqeq12d	$$⊢y={1_R}^{{\mathrm{*}}_R}\to \left({\left(1_R{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{1_R}^{{\mathrm{*}}_R}\leftrightarrow {\left(1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}\right)}^{{\mathrm{*}}_R}={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}{\cdot }_R{1_R}^{{\mathrm{*}}_R}\right)$$
59	53 58	rspc2va	$$⊢\left(\left(1_R\in {\mathrm{Base}}_R\wedge {1_R}^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R\right)\wedge \forall x\in {\mathrm{Base}}_R\forall y\in {\mathrm{Base}}_R{\left(x{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{x}^{{\mathrm{*}}_R}\right)\to {\left(1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}\right)}^{{\mathrm{*}}_R}={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}{\cdot }_R{1_R}^{{\mathrm{*}}_R}$$
60	32 40 50 59	syl21anc	$$⊢\phi \to {\left(1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}\right)}^{{\mathrm{*}}_R}={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}{\cdot }_R{1_R}^{{\mathrm{*}}_R}$$
61	34 60	eqtr4d	$$⊢\phi \to 1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}={\left(1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}\right)}^{{\mathrm{*}}_R}$$
62	10 14 11	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge {1_R}^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R\right)\to 1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}={1_R}^{{\mathrm{*}}_R}$$
63	5 40 62	syl2anc	$$⊢\phi \to 1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}={1_R}^{{\mathrm{*}}_R}$$
64	63	fveq2d	$$⊢\phi \to {\left(1_R{\cdot }_R{1_R}^{{\mathrm{*}}_R}\right)}^{{\mathrm{*}}_R}={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
65	61 63 64	3eqtr3d	$$⊢\phi \to {1_R}^{{\mathrm{*}}_R}={{1_R}^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
66		eqid	$$⊢{\mathrm{*}}_R={\mathrm{*}}_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}^{{\mathrm{*}}_R}$$
69	32 68	syl	$$⊢\phi \to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(1_R\right)={1_R}^{{\mathrm{*}}_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)}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{x}^{{\mathrm{*}}_R}$$
72	10 14 12 15	opprmul	$$⊢x^{{\mathrm{*}}_R}{\cdot }_{{opp}_r\left(R\right)}{y}^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}{\cdot }_R{x}^{{\mathrm{*}}_R}$$
73	71 72	eqtr4di	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to {\left(x{\cdot }_{R}y\right)}^{{\mathrm{*}}_R}=x^{{\mathrm{*}}_R}{\cdot }_{{opp}_r\left(R\right)}{y}^{{\mathrm{*}}_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)}^{{\mathrm{*}}_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)}^{{\mathrm{*}}_R}$$
79	10 66 67	stafval	$$⊢x\in {\mathrm{Base}}_R\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(x\right)=x^{{\mathrm{*}}_R}$$
80	10 66 67	stafval	$$⊢y\in {\mathrm{Base}}_R\to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)\left(y\right)=y^{{\mathrm{*}}_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^{{\mathrm{*}}_R}{\cdot }_{{opp}_r\left(R\right)}{y}^{{\mathrm{*}}_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^{{\mathrm{*}}_R}{\cdot }_{{opp}_r\left(R\right)}{y}^{{\mathrm{*}}_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^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R$$
88	10 66 67	staffval	$$⊢{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)=\left(x\in {\mathrm{Base}}_R⟼x^{{\mathrm{*}}_R}\right)$$
89	87 88	fmptd	$$⊢\phi \to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right):{\mathrm{Base}}_R⟶{\mathrm{Base}}_R$$
90	7	3expib	$$⊢\phi \to \left(\left(x\in K\wedge y\in K\right)\to \underset{\dot{}}{\ast }\left(x\underset{\dot{}}{+}y\right)=\underset{\dot{}}{\ast }\left(x\right)\underset{\dot{}}{+}\underset{\dot{}}{\ast }\left(y\right)\right)$$
91	2	oveqd	$$⊢\phi \to x\underset{\dot{}}{+}y=x{+}_{R}y$$
92	4 91	fveq12d	$$⊢\phi \to \underset{\dot{}}{\ast }\left(x\underset{\dot{}}{+}y\right)={\left(x{+}_{R}y\right)}^{{\mathrm{*}}_R}$$
93	2 24 46	oveq123d	$$⊢\phi \to \underset{\dot{}}{\ast }\left(x\right)\underset{\dot{}}{+}\underset{\dot{}}{\ast }\left(y\right)=x^{{\mathrm{*}}_R}{+}_R{y}^{{\mathrm{*}}_R}$$
94	92 93	eqeq12d	$$⊢\phi \to \left(\underset{\dot{}}{\ast }\left(x\underset{\dot{}}{+}y\right)=\underset{\dot{}}{\ast }\left(x\right)\underset{\dot{}}{+}\underset{\dot{}}{\ast }\left(y\right)\leftrightarrow {\left(x{+}_{R}y\right)}^{{\mathrm{*}}_R}=x^{{\mathrm{*}}_R}{+}_R{y}^{{\mathrm{*}}_R}\right)$$
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)}^{{\mathrm{*}}_R}=x^{{\mathrm{*}}_R}{+}_R{y}^{{\mathrm{*}}_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)}^{{\mathrm{*}}_R}=x^{{\mathrm{*}}_R}{+}_R{y}^{{\mathrm{*}}_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)}^{{\mathrm{*}}_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)}^{{\mathrm{*}}_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^{{\mathrm{*}}_R}{+}_R{y}^{{\mathrm{*}}_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^{{\mathrm{*}}_R}{+}_R{y}^{{\mathrm{*}}_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^{{\mathrm{*}}_R}\right)$$
107	106	fmpt	$$⊢\forall y\in {\mathrm{Base}}_R{y}^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R\leftrightarrow {\ast }_{\mathrm{𝑟𝑓}}\left(R\right):{\mathrm{Base}}_R⟶{\mathrm{Base}}_R$$
108	89 107	sylibr	$$⊢\phi \to \forall y\in {\mathrm{Base}}_R{y}^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R$$
109	108	r19.21bi	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_R\right)\to y^{{\mathrm{*}}_R}\in {\mathrm{Base}}_R$$
110		id	$$⊢x=y\to x=y$$
111		fveq2	$$⊢x=y\to x^{{\mathrm{*}}_R}=y^{{\mathrm{*}}_R}$$
112	111	fveq2d	$$⊢x=y\to {x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}={y^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
113	110 112	eqeq12d	$$⊢x=y\to \left(x={x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}\leftrightarrow y={y^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}\right)$$
114	113	rspccva	$$⊢\left(\forall x\in {\mathrm{Base}}_{R}x={x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}\wedge y\in {\mathrm{Base}}_R\right)\to y={y^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
115	30 114	sylan	$$⊢\left(\phi \wedge y\in {\mathrm{Base}}_R\right)\to y={y^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
116	115	adantrl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to y={y^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
117		fveq2	$$⊢x=y^{{\mathrm{*}}_R}\to x^{{\mathrm{*}}_R}={y^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
118	117	eqeq2d	$$⊢x=y^{{\mathrm{*}}_R}\to \left(y=x^{{\mathrm{*}}_R}\leftrightarrow y={y^{{\mathrm{*}}_R}}^{{\mathrm{*}}_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^{{\mathrm{*}}_R}\to y=x^{{\mathrm{*}}_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^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
121		fveq2	$$⊢y=x^{{\mathrm{*}}_R}\to y^{{\mathrm{*}}_R}={x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_R}$$
122	121	eqeq2d	$$⊢y=x^{{\mathrm{*}}_R}\to \left(x=y^{{\mathrm{*}}_R}\leftrightarrow x={x^{{\mathrm{*}}_R}}^{{\mathrm{*}}_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^{{\mathrm{*}}_R}\to x=y^{{\mathrm{*}}_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^{{\mathrm{*}}_R}\leftrightarrow y=x^{{\mathrm{*}}_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^{{\mathrm{*}}_R}\right)\right)$$
126	125	simprd	$$⊢\phi \to {{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)}^{-1}=\left(y\in {\mathrm{Base}}_R⟼y^{{\mathrm{*}}_R}\right)$$
127	106 126	eqtr4id	$$⊢\phi \to {\ast }_{\mathrm{𝑟𝑓}}\left(R\right)={{\ast }_{\mathrm{𝑟𝑓}}\left(R\right)}^{-1}$$
128	12 67	issrng	$$⊢R\in \mathrm{*-Ring}\leftrightarrow \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}$$