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 )