# 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 = ( Base ` R )`
idsrngd.c
`|- .* = ( *r ` R )`
idsrngd.r
`|- ( ph -> R e. CRing )`
idsrngd.i
`|- ( ( ph /\ x e. B ) -> ( .* ` x ) = x )`
Assertion idsrngd
`|- ( ph -> R e. *Ring )`

### Proof

Step Hyp Ref Expression
1 idsrngd.k
` |-  B = ( Base ` R )`
2 idsrngd.c
` |-  .* = ( *r ` R )`
3 idsrngd.r
` |-  ( ph -> R e. CRing )`
4 idsrngd.i
` |-  ( ( ph /\ x e. B ) -> ( .* ` x ) = x )`
5 1 a1i
` |-  ( ph -> B = ( Base ` R ) )`
6 eqidd
` |-  ( ph -> ( +g ` R ) = ( +g ` R ) )`
7 eqidd
` |-  ( ph -> ( .r ` R ) = ( .r ` R ) )`
8 2 a1i
` |-  ( ph -> .* = ( *r ` R ) )`
9 crngring
` |-  ( R e. CRing -> R e. Ring )`
10 3 9 syl
` |-  ( ph -> R e. Ring )`
11 4 ralrimiva
` |-  ( ph -> A. x e. B ( .* ` x ) = x )`
` |-  ( ( ph /\ a e. B ) -> A. x e. B ( .* ` x ) = x )`
13 simpr
` |-  ( ( ph /\ a e. B ) -> a e. B )`
14 simpr
` |-  ( ( ( ph /\ a e. B ) /\ x = a ) -> x = a )`
15 14 fveq2d
` |-  ( ( ( ph /\ a e. B ) /\ x = a ) -> ( .* ` x ) = ( .* ` a ) )`
16 15 14 eqeq12d
` |-  ( ( ( ph /\ a e. B ) /\ x = a ) -> ( ( .* ` x ) = x <-> ( .* ` a ) = a ) )`
17 13 16 rspcdv
` |-  ( ( ph /\ a e. B ) -> ( A. x e. B ( .* ` x ) = x -> ( .* ` a ) = a ) )`
18 12 17 mpd
` |-  ( ( ph /\ a e. B ) -> ( .* ` a ) = a )`
19 18 13 eqeltrd
` |-  ( ( ph /\ a e. B ) -> ( .* ` a ) e. B )`
` |-  ( ( ph /\ b e. B ) -> A. x e. B ( .* ` x ) = x )`
` |-  ( ( ph /\ a e. B /\ b e. B ) -> A. x e. B ( .* ` x ) = x )`
22 ringgrp
` |-  ( R e. Ring -> R e. Grp )`
23 10 22 syl
` |-  ( ph -> R e. Grp )`
24 eqid
` |-  ( +g ` R ) = ( +g ` R )`
25 1 24 grpcl
` |-  ( ( R e. Grp /\ a e. B /\ b e. B ) -> ( a ( +g ` R ) b ) e. B )`
26 23 25 syl3an1
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( a ( +g ` R ) b ) e. B )`
27 simpr
` |-  ( ( ( ph /\ a e. B /\ b e. B ) /\ x = ( a ( +g ` R ) b ) ) -> x = ( a ( +g ` R ) b ) )`
28 27 fveq2d
` |-  ( ( ( ph /\ a e. B /\ b e. B ) /\ x = ( a ( +g ` R ) b ) ) -> ( .* ` x ) = ( .* ` ( a ( +g ` R ) b ) ) )`
29 28 27 eqeq12d
` |-  ( ( ( ph /\ a e. B /\ b e. B ) /\ x = ( a ( +g ` R ) b ) ) -> ( ( .* ` x ) = x <-> ( .* ` ( a ( +g ` R ) b ) ) = ( a ( +g ` R ) b ) ) )`
30 26 29 rspcdv
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( A. x e. B ( .* ` x ) = x -> ( .* ` ( a ( +g ` R ) b ) ) = ( a ( +g ` R ) b ) ) )`
31 21 30 mpd
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( .* ` ( a ( +g ` R ) b ) ) = ( a ( +g ` R ) b ) )`
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( .* ` a ) = a )`
33 simpr
` |-  ( ( ph /\ b e. B ) -> b e. B )`
34 simpr
` |-  ( ( ( ph /\ b e. B ) /\ x = b ) -> x = b )`
35 34 fveq2d
` |-  ( ( ( ph /\ b e. B ) /\ x = b ) -> ( .* ` x ) = ( .* ` b ) )`
36 35 34 eqeq12d
` |-  ( ( ( ph /\ b e. B ) /\ x = b ) -> ( ( .* ` x ) = x <-> ( .* ` b ) = b ) )`
37 33 36 rspcdv
` |-  ( ( ph /\ b e. B ) -> ( A. x e. B ( .* ` x ) = x -> ( .* ` b ) = b ) )`
38 20 37 mpd
` |-  ( ( ph /\ b e. B ) -> ( .* ` b ) = b )`
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( .* ` b ) = b )`
40 32 39 oveq12d
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( ( .* ` a ) ( +g ` R ) ( .* ` b ) ) = ( a ( +g ` R ) b ) )`
41 31 40 eqtr4d
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( .* ` ( a ( +g ` R ) b ) ) = ( ( .* ` a ) ( +g ` R ) ( .* ` b ) ) )`
42 eqid
` |-  ( .r ` R ) = ( .r ` R )`
43 1 42 crngcom
` |-  ( ( R e. CRing /\ a e. B /\ b e. B ) -> ( a ( .r ` R ) b ) = ( b ( .r ` R ) a ) )`
44 3 43 syl3an1
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( a ( .r ` R ) b ) = ( b ( .r ` R ) a ) )`
45 1 42 ringcl
` |-  ( ( R e. Ring /\ a e. B /\ b e. B ) -> ( a ( .r ` R ) b ) e. B )`
46 10 45 syl3an1
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( a ( .r ` R ) b ) e. B )`
47 simpr
` |-  ( ( ( ph /\ a e. B /\ b e. B ) /\ x = ( a ( .r ` R ) b ) ) -> x = ( a ( .r ` R ) b ) )`
48 47 fveq2d
` |-  ( ( ( ph /\ a e. B /\ b e. B ) /\ x = ( a ( .r ` R ) b ) ) -> ( .* ` x ) = ( .* ` ( a ( .r ` R ) b ) ) )`
49 48 47 eqeq12d
` |-  ( ( ( ph /\ a e. B /\ b e. B ) /\ x = ( a ( .r ` R ) b ) ) -> ( ( .* ` x ) = x <-> ( .* ` ( a ( .r ` R ) b ) ) = ( a ( .r ` R ) b ) ) )`
50 46 49 rspcdv
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( A. x e. B ( .* ` x ) = x -> ( .* ` ( a ( .r ` R ) b ) ) = ( a ( .r ` R ) b ) ) )`
51 21 50 mpd
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( .* ` ( a ( .r ` R ) b ) ) = ( a ( .r ` R ) b ) )`
52 39 32 oveq12d
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( ( .* ` b ) ( .r ` R ) ( .* ` a ) ) = ( b ( .r ` R ) a ) )`
53 44 51 52 3eqtr4d
` |-  ( ( ph /\ a e. B /\ b e. B ) -> ( .* ` ( a ( .r ` R ) b ) ) = ( ( .* ` b ) ( .r ` R ) ( .* ` a ) ) )`
54 18 fveq2d
` |-  ( ( ph /\ a e. B ) -> ( .* ` ( .* ` a ) ) = ( .* ` a ) )`
55 54 18 eqtrd
` |-  ( ( ph /\ a e. B ) -> ( .* ` ( .* ` a ) ) = a )`
56 5 6 7 8 10 19 41 53 55 issrngd
` |-  ( ph -> R e. *Ring )`