# Metamath Proof Explorer

## 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
idsrngd.r ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
idsrngd.i
Assertion idsrngd ${⊢}{\phi }\to {R}\in \mathrm{*-Ring}$

### Proof

Step Hyp Ref Expression
1 idsrngd.k ${⊢}{B}={\mathrm{Base}}_{{R}}$
2 idsrngd.c
3 idsrngd.r ${⊢}{\phi }\to {R}\in \mathrm{CRing}$
4 idsrngd.i
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
9 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
10 3 9 syl ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
11 4 ralrimiva
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
16 15 14 eqeq12d
17 13 16 rspcdv
18 12 17 mpd
19 18 13 eqeltrd
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
29 28 27 eqeq12d
30 26 29 rspcdv
31 21 30 mpd
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
36 35 34 eqeq12d
37 33 36 rspcdv
38 20 37 mpd
40 32 39 oveq12d
41 31 40 eqtr4d
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
49 48 47 eqeq12d
50 46 49 rspcdv
51 21 50 mpd
52 39 32 oveq12d
53 44 51 52 3eqtr4d
54 18 fveq2d
55 54 18 eqtrd
56 5 6 7 8 10 19 41 53 55 issrngd ${⊢}{\phi }\to {R}\in \mathrm{*-Ring}$