# 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 𝐵 = ( Base ‘ 𝑅 )
idsrngd.c = ( *𝑟𝑅 )
idsrngd.r ( 𝜑𝑅 ∈ CRing )
idsrngd.i ( ( 𝜑𝑥𝐵 ) → ( 𝑥 ) = 𝑥 )
Assertion idsrngd ( 𝜑𝑅 ∈ *-Ring )

### Proof

Step Hyp Ref Expression
1 idsrngd.k 𝐵 = ( Base ‘ 𝑅 )
2 idsrngd.c = ( *𝑟𝑅 )
3 idsrngd.r ( 𝜑𝑅 ∈ CRing )
4 idsrngd.i ( ( 𝜑𝑥𝐵 ) → ( 𝑥 ) = 𝑥 )
5 1 a1i ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
6 eqidd ( 𝜑 → ( +g𝑅 ) = ( +g𝑅 ) )
7 eqidd ( 𝜑 → ( .r𝑅 ) = ( .r𝑅 ) )
8 2 a1i ( 𝜑 = ( *𝑟𝑅 ) )
9 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10 3 9 syl ( 𝜑𝑅 ∈ Ring )
11 4 ralrimiva ( 𝜑 → ∀ 𝑥𝐵 ( 𝑥 ) = 𝑥 )
12 11 adantr ( ( 𝜑𝑎𝐵 ) → ∀ 𝑥𝐵 ( 𝑥 ) = 𝑥 )
13 simpr ( ( 𝜑𝑎𝐵 ) → 𝑎𝐵 )
14 simpr ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑥 = 𝑎 ) → 𝑥 = 𝑎 )
15 14 fveq2d ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑥 = 𝑎 ) → ( 𝑥 ) = ( 𝑎 ) )
16 15 14 eqeq12d ( ( ( 𝜑𝑎𝐵 ) ∧ 𝑥 = 𝑎 ) → ( ( 𝑥 ) = 𝑥 ↔ ( 𝑎 ) = 𝑎 ) )
17 13 16 rspcdv ( ( 𝜑𝑎𝐵 ) → ( ∀ 𝑥𝐵 ( 𝑥 ) = 𝑥 → ( 𝑎 ) = 𝑎 ) )
18 12 17 mpd ( ( 𝜑𝑎𝐵 ) → ( 𝑎 ) = 𝑎 )
19 18 13 eqeltrd ( ( 𝜑𝑎𝐵 ) → ( 𝑎 ) ∈ 𝐵 )
20 11 adantr ( ( 𝜑𝑏𝐵 ) → ∀ 𝑥𝐵 ( 𝑥 ) = 𝑥 )
21 20 3adant2 ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ∀ 𝑥𝐵 ( 𝑥 ) = 𝑥 )
22 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
23 10 22 syl ( 𝜑𝑅 ∈ Grp )
24 eqid ( +g𝑅 ) = ( +g𝑅 )
25 1 24 grpcl ( ( 𝑅 ∈ Grp ∧ 𝑎𝐵𝑏𝐵 ) → ( 𝑎 ( +g𝑅 ) 𝑏 ) ∈ 𝐵 )
26 23 25 syl3an1 ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( 𝑎 ( +g𝑅 ) 𝑏 ) ∈ 𝐵 )
27 simpr ( ( ( 𝜑𝑎𝐵𝑏𝐵 ) ∧ 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) ) → 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) )
28 27 fveq2d ( ( ( 𝜑𝑎𝐵𝑏𝐵 ) ∧ 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) ) → ( 𝑥 ) = ( ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) )
29 28 27 eqeq12d ( ( ( 𝜑𝑎𝐵𝑏𝐵 ) ∧ 𝑥 = ( 𝑎 ( +g𝑅 ) 𝑏 ) ) → ( ( 𝑥 ) = 𝑥 ↔ ( ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( 𝑎 ( +g𝑅 ) 𝑏 ) ) )
30 26 29 rspcdv ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( ∀ 𝑥𝐵 ( 𝑥 ) = 𝑥 → ( ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( 𝑎 ( +g𝑅 ) 𝑏 ) ) )
31 21 30 mpd ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( 𝑎 ( +g𝑅 ) 𝑏 ) )
32 18 3adant3 ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( 𝑎 ) = 𝑎 )
33 simpr ( ( 𝜑𝑏𝐵 ) → 𝑏𝐵 )
34 simpr ( ( ( 𝜑𝑏𝐵 ) ∧ 𝑥 = 𝑏 ) → 𝑥 = 𝑏 )
35 34 fveq2d ( ( ( 𝜑𝑏𝐵 ) ∧ 𝑥 = 𝑏 ) → ( 𝑥 ) = ( 𝑏 ) )
36 35 34 eqeq12d ( ( ( 𝜑𝑏𝐵 ) ∧ 𝑥 = 𝑏 ) → ( ( 𝑥 ) = 𝑥 ↔ ( 𝑏 ) = 𝑏 ) )
37 33 36 rspcdv ( ( 𝜑𝑏𝐵 ) → ( ∀ 𝑥𝐵 ( 𝑥 ) = 𝑥 → ( 𝑏 ) = 𝑏 ) )
38 20 37 mpd ( ( 𝜑𝑏𝐵 ) → ( 𝑏 ) = 𝑏 )
39 38 3adant2 ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( 𝑏 ) = 𝑏 )
40 32 39 oveq12d ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( ( 𝑎 ) ( +g𝑅 ) ( 𝑏 ) ) = ( 𝑎 ( +g𝑅 ) 𝑏 ) )
41 31 40 eqtr4d ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( ‘ ( 𝑎 ( +g𝑅 ) 𝑏 ) ) = ( ( 𝑎 ) ( +g𝑅 ) ( 𝑏 ) ) )
42 eqid ( .r𝑅 ) = ( .r𝑅 )
43 1 42 crngcom ( ( 𝑅 ∈ CRing ∧ 𝑎𝐵𝑏𝐵 ) → ( 𝑎 ( .r𝑅 ) 𝑏 ) = ( 𝑏 ( .r𝑅 ) 𝑎 ) )
44 3 43 syl3an1 ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( 𝑎 ( .r𝑅 ) 𝑏 ) = ( 𝑏 ( .r𝑅 ) 𝑎 ) )
45 1 42 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑎𝐵𝑏𝐵 ) → ( 𝑎 ( .r𝑅 ) 𝑏 ) ∈ 𝐵 )
46 10 45 syl3an1 ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( 𝑎 ( .r𝑅 ) 𝑏 ) ∈ 𝐵 )
47 simpr ( ( ( 𝜑𝑎𝐵𝑏𝐵 ) ∧ 𝑥 = ( 𝑎 ( .r𝑅 ) 𝑏 ) ) → 𝑥 = ( 𝑎 ( .r𝑅 ) 𝑏 ) )
48 47 fveq2d ( ( ( 𝜑𝑎𝐵𝑏𝐵 ) ∧ 𝑥 = ( 𝑎 ( .r𝑅 ) 𝑏 ) ) → ( 𝑥 ) = ( ‘ ( 𝑎 ( .r𝑅 ) 𝑏 ) ) )
49 48 47 eqeq12d ( ( ( 𝜑𝑎𝐵𝑏𝐵 ) ∧ 𝑥 = ( 𝑎 ( .r𝑅 ) 𝑏 ) ) → ( ( 𝑥 ) = 𝑥 ↔ ( ‘ ( 𝑎 ( .r𝑅 ) 𝑏 ) ) = ( 𝑎 ( .r𝑅 ) 𝑏 ) ) )
50 46 49 rspcdv ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( ∀ 𝑥𝐵 ( 𝑥 ) = 𝑥 → ( ‘ ( 𝑎 ( .r𝑅 ) 𝑏 ) ) = ( 𝑎 ( .r𝑅 ) 𝑏 ) ) )
51 21 50 mpd ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( ‘ ( 𝑎 ( .r𝑅 ) 𝑏 ) ) = ( 𝑎 ( .r𝑅 ) 𝑏 ) )
52 39 32 oveq12d ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( ( 𝑏 ) ( .r𝑅 ) ( 𝑎 ) ) = ( 𝑏 ( .r𝑅 ) 𝑎 ) )
53 44 51 52 3eqtr4d ( ( 𝜑𝑎𝐵𝑏𝐵 ) → ( ‘ ( 𝑎 ( .r𝑅 ) 𝑏 ) ) = ( ( 𝑏 ) ( .r𝑅 ) ( 𝑎 ) ) )
54 18 fveq2d ( ( 𝜑𝑎𝐵 ) → ( ‘ ( 𝑎 ) ) = ( 𝑎 ) )
55 54 18 eqtrd ( ( 𝜑𝑎𝐵 ) → ( ‘ ( 𝑎 ) ) = 𝑎 )
56 5 6 7 8 10 19 41 53 55 issrngd ( 𝜑𝑅 ∈ *-Ring )