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 )
12 11 adantr
 |-  ( ( 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 )
20 11 adantr
 |-  ( ( ph /\ b e. B ) -> A. x e. B ( .* ` x ) = x )
21 20 3adant2
 |-  ( ( 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 ) )
32 18 3adant3
 |-  ( ( 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 )
39 38 3adant2
 |-  ( ( 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 )