Theorem idsrngd

Description: A commutative ring is a star ring when the conjugate operation is the identity. (Contributed by Thierry Arnoux, 19-Apr-2019)

	Ref	Expression
Hypotheses	idsrngd.k	$$⊢B={\mathrm{Base}}_R$$
	idsrngd.c	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
	idsrngd.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	idsrngd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{\ast }\left(x\right)=x$$
Assertion	idsrngd	$$⊢\phi \to R\in \mathrm{*-Ring}$$

Proof

Step	Hyp	Ref	Expression
1		idsrngd.k	$$⊢B={\mathrm{Base}}_R$$
2		idsrngd.c	$$⊢\underset{\dot{}}{\ast }={\mathrm{*}}_R$$
3		idsrngd.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4		idsrngd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{\ast }\left(x\right)=x$$
5	1	a1i	$$⊢\phi \to B={\mathrm{Base}}_R$$
6		eqidd	$$⊢\phi \to {+}_R={+}_R$$
7		eqidd	$$⊢\phi \to {\cdot }_R={\cdot }_R$$
8	2	a1i	$$⊢\phi \to \underset{\dot{}}{\ast }={\mathrm{*}}_R$$
9		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
10	3 9	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
11	4	ralrimiva	$$⊢\phi \to \forall x\in B\underset{\dot{}}{\ast }\left(x\right)=x$$
12	11	adantr	$$⊢\left(\phi \wedge a\in B\right)\to \forall x\in B\underset{\dot{}}{\ast }\left(x\right)=x$$
13		simpr	$$⊢\left(\phi \wedge a\in B\right)\to a\in B$$
14		simpr	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge x=a\right)\to x=a$$
15	14	fveq2d	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge x=a\right)\to \underset{\dot{}}{\ast }\left(x\right)=\underset{\dot{}}{\ast }\left(a\right)$$
16	15 14	eqeq12d	$$⊢\left(\left(\phi \wedge a\in B\right)\wedge x=a\right)\to \left(\underset{\dot{}}{\ast }\left(x\right)=x\leftrightarrow \underset{\dot{}}{\ast }\left(a\right)=a\right)$$
17	13 16	rspcdv	$$⊢\left(\phi \wedge a\in B\right)\to \left(\forall x\in B\underset{\dot{}}{\ast }\left(x\right)=x\to \underset{\dot{}}{\ast }\left(a\right)=a\right)$$
18	12 17	mpd	$$⊢\left(\phi \wedge a\in B\right)\to \underset{\dot{}}{\ast }\left(a\right)=a$$
19	18 13	eqeltrd	$$⊢\left(\phi \wedge a\in B\right)\to \underset{\dot{}}{\ast }\left(a\right)\in B$$
20	11	adantr	$$⊢\left(\phi \wedge b\in B\right)\to \forall x\in B\underset{\dot{}}{\ast }\left(x\right)=x$$
21	20	3adant2	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \forall x\in B\underset{\dot{}}{\ast }\left(x\right)=x$$
22		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
23	10 22	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
24		eqid	$$⊢{+}_R={+}_R$$
25	1 24	grpcl	$$⊢\left(R\in \mathrm{Grp}\wedge a\in B\wedge b\in B\right)\to a{+}_{R}b\in B$$
26	23 25	syl3an1	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to a{+}_{R}b\in B$$
27		simpr	$$⊢\left(\left(\phi \wedge a\in B\wedge b\in B\right)\wedge x=a{+}_{R}b\right)\to x=a{+}_{R}b$$
28	27	fveq2d	$$⊢\left(\left(\phi \wedge a\in B\wedge b\in B\right)\wedge x=a{+}_{R}b\right)\to \underset{\dot{}}{\ast }\left(x\right)=\underset{\dot{}}{\ast }\left(a{+}_{R}b\right)$$
29	28 27	eqeq12d	$$⊢\left(\left(\phi \wedge a\in B\wedge b\in B\right)\wedge x=a{+}_{R}b\right)\to \left(\underset{\dot{}}{\ast }\left(x\right)=x\leftrightarrow \underset{\dot{}}{\ast }\left(a{+}_{R}b\right)=a{+}_{R}b\right)$$
30	26 29	rspcdv	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \left(\forall x\in B\underset{\dot{}}{\ast }\left(x\right)=x\to \underset{\dot{}}{\ast }\left(a{+}_{R}b\right)=a{+}_{R}b\right)$$
31	21 30	mpd	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \underset{\dot{}}{\ast }\left(a{+}_{R}b\right)=a{+}_{R}b$$
32	18	3adant3	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \underset{\dot{}}{\ast }\left(a\right)=a$$
33		simpr	$$⊢\left(\phi \wedge b\in B\right)\to b\in B$$
34		simpr	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge x=b\right)\to x=b$$
35	34	fveq2d	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge x=b\right)\to \underset{\dot{}}{\ast }\left(x\right)=\underset{\dot{}}{\ast }\left(b\right)$$
36	35 34	eqeq12d	$$⊢\left(\left(\phi \wedge b\in B\right)\wedge x=b\right)\to \left(\underset{\dot{}}{\ast }\left(x\right)=x\leftrightarrow \underset{\dot{}}{\ast }\left(b\right)=b\right)$$
37	33 36	rspcdv	$$⊢\left(\phi \wedge b\in B\right)\to \left(\forall x\in B\underset{\dot{}}{\ast }\left(x\right)=x\to \underset{\dot{}}{\ast }\left(b\right)=b\right)$$
38	20 37	mpd	$$⊢\left(\phi \wedge b\in B\right)\to \underset{\dot{}}{\ast }\left(b\right)=b$$
39	38	3adant2	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \underset{\dot{}}{\ast }\left(b\right)=b$$
40	32 39	oveq12d	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \underset{\dot{}}{\ast }\left(a\right){+}_R\underset{\dot{}}{\ast }\left(b\right)=a{+}_{R}b$$
41	31 40	eqtr4d	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \underset{\dot{}}{\ast }\left(a{+}_{R}b\right)=\underset{\dot{}}{\ast }\left(a\right){+}_R\underset{\dot{}}{\ast }\left(b\right)$$
42		eqid	$$⊢{\cdot }_R={\cdot }_R$$
43	1 42	crngcom	$$⊢\left(R\in \mathrm{CRing}\wedge a\in B\wedge b\in B\right)\to a{\cdot }_{R}b=b{\cdot }_{R}a$$
44	3 43	syl3an1	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to a{\cdot }_{R}b=b{\cdot }_{R}a$$
45	1 42	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge a\in B\wedge b\in B\right)\to a{\cdot }_{R}b\in B$$
46	10 45	syl3an1	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to a{\cdot }_{R}b\in B$$
47		simpr	$$⊢\left(\left(\phi \wedge a\in B\wedge b\in B\right)\wedge x=a{\cdot }_{R}b\right)\to x=a{\cdot }_{R}b$$
48	47	fveq2d	$$⊢\left(\left(\phi \wedge a\in B\wedge b\in B\right)\wedge x=a{\cdot }_{R}b\right)\to \underset{\dot{}}{\ast }\left(x\right)=\underset{\dot{}}{\ast }\left(a{\cdot }_{R}b\right)$$
49	48 47	eqeq12d	$$⊢\left(\left(\phi \wedge a\in B\wedge b\in B\right)\wedge x=a{\cdot }_{R}b\right)\to \left(\underset{\dot{}}{\ast }\left(x\right)=x\leftrightarrow \underset{\dot{}}{\ast }\left(a{\cdot }_{R}b\right)=a{\cdot }_{R}b\right)$$
50	46 49	rspcdv	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \left(\forall x\in B\underset{\dot{}}{\ast }\left(x\right)=x\to \underset{\dot{}}{\ast }\left(a{\cdot }_{R}b\right)=a{\cdot }_{R}b\right)$$
51	21 50	mpd	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \underset{\dot{}}{\ast }\left(a{\cdot }_{R}b\right)=a{\cdot }_{R}b$$
52	39 32	oveq12d	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \underset{\dot{}}{\ast }\left(b\right){\cdot }_R\underset{\dot{}}{\ast }\left(a\right)=b{\cdot }_{R}a$$
53	44 51 52	3eqtr4d	$$⊢\left(\phi \wedge a\in B\wedge b\in B\right)\to \underset{\dot{}}{\ast }\left(a{\cdot }_{R}b\right)=\underset{\dot{}}{\ast }\left(b\right){\cdot }_R\underset{\dot{}}{\ast }\left(a\right)$$
54	18	fveq2d	$$⊢\left(\phi \wedge a\in B\right)\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(a\right)\right)=\underset{\dot{}}{\ast }\left(a\right)$$
55	54 18	eqtrd	$$⊢\left(\phi \wedge a\in B\right)\to \underset{\dot{}}{\ast }\left(\underset{\dot{}}{\ast }\left(a\right)\right)=a$$
56	5 6 7 8 10 19 41 53 55	issrngd	$$⊢\phi \to R\in \mathrm{*-Ring}$$