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 )