Metamath Proof Explorer

Theorem issrngd

Description: Properties that determine a star ring. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 6-Oct-2015)

Ref Expression
Hypotheses issrngd.k ⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝑅 ) )
issrngd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
issrngd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
issrngd.c ⊢ ( 𝜑 → ∗ = ( *𝑟 ‘ 𝑅 ) )
issrngd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
issrngd.cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ∗ ‘ 𝑥 ) ∈ 𝐾 )
issrngd.dp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( ∗ ‘ ( 𝑥 + 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) + ( ∗ ‘ 𝑦 ) ) )
issrngd.dt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( ∗ ‘ ( 𝑥 · 𝑦 ) ) = ( ( ∗ ‘ 𝑦 ) · ( ∗ ‘ 𝑥 ) ) )
issrngd.id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ∗ ‘ ( ∗ ‘ 𝑥 ) ) = 𝑥 )
Assertion issrngd ( 𝜑 → 𝑅 ∈ *-Ring )

Proof

Step Hyp Ref Expression
1 issrngd.k ⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝑅 ) )
2 issrngd.p ⊢ ( 𝜑 → + = ( +g ‘ 𝑅 ) )
3 issrngd.t ⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
4 issrngd.c ⊢ ( 𝜑 → ∗ = ( *𝑟 ‘ 𝑅 ) )
5 issrngd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 issrngd.cl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ∗ ‘ 𝑥 ) ∈ 𝐾 )
7 issrngd.dp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( ∗ ‘ ( 𝑥 + 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) + ( ∗ ‘ 𝑦 ) ) )
8 issrngd.dt ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( ∗ ‘ ( 𝑥 · 𝑦 ) ) = ( ( ∗ ‘ 𝑦 ) · ( ∗ ‘ 𝑥 ) ) )
9 issrngd.id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ∗ ‘ ( ∗ ‘ 𝑥 ) ) = 𝑥 )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
12 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
13 12 11 oppr1 ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ ( oppr ‘ 𝑅 ) )
14 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
15 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
16 12 opprring ⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
17 5 16 syl ⊢ ( 𝜑 → ( oppr ‘ 𝑅 ) ∈ Ring )
18 id ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → 𝑥 = ( 1r ‘ 𝑅 ) )
19 fveq2 ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
20 19 fveq2d ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
21 18 20 eqeq12d ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) ↔ ( 1r ‘ 𝑅 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ) )
22 9 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 → ( ∗ ‘ ( ∗ ‘ 𝑥 ) ) = 𝑥 ) )
23 1 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 ↔ 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
24 4 fveq1d ⊢ ( 𝜑 → ( ∗ ‘ 𝑥 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) )
25 4 24 fveq12d ⊢ ( 𝜑 → ( ∗ ‘ ( ∗ ‘ 𝑥 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
26 25 eqeq1d ⊢ ( 𝜑 → ( ( ∗ ‘ ( ∗ ‘ 𝑥 ) ) = 𝑥 ↔ ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) = 𝑥 ) )
27 22 23 26 3imtr3d ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) = 𝑥 ) )
28 27 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) = 𝑥 )
29 28 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
31 10 11 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
32 5 31 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
33 21 30 32 rspcdva ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
34 33 oveq1d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
35 19 eleq1d ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ↔ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) ) )
36 6 ex ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 → ( ∗ ‘ 𝑥 ) ∈ 𝐾 ) )
37 24 1 eleq12d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑥 ) ∈ 𝐾 ↔ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) )
38 36 23 37 3imtr3d ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) )
39 38 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
40 35 39 32 rspcdva ⊢ ( 𝜑 → ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
41 8 3expib ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( ∗ ‘ ( 𝑥 · 𝑦 ) ) = ( ( ∗ ‘ 𝑦 ) · ( ∗ ‘ 𝑥 ) ) ) )
42 1 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 ↔ 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
43 23 42 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) )
44 3 oveqd ⊢ ( 𝜑 → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
45 4 44 fveq12d ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑥 · 𝑦 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
46 4 fveq1d ⊢ ( 𝜑 → ( ∗ ‘ 𝑦 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) )
47 3 46 24 oveq123d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑦 ) · ( ∗ ‘ 𝑥 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
48 45 47 eqeq12d ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝑥 · 𝑦 ) ) = ( ( ∗ ‘ 𝑦 ) · ( ∗ ‘ 𝑥 ) ) ↔ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) ) )
49 41 43 48 3imtr3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) ) )
50 49 ralrimivv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
51 fvoveq1 ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) ) )
52 19 oveq2d ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
53 51 52 eqeq12d ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) ↔ ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ) )
54 oveq2 ⊢ ( 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
55 54 fveq2d ⊢ ( 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ) )
56 fveq2 ⊢ ( 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
57 56 oveq1d ⊢ ( 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) → ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
58 55 57 eqeq12d ⊢ ( 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) → ( ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ↔ ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ) )
59 53 58 rspc2va ⊢ ( ( ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
60 32 40 50 59 syl21anc ⊢ ( 𝜑 → ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
61 34 60 eqtr4d ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ) )
62 10 14 11 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
63 5 40 62 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
64 63 fveq2d ⊢ ( 𝜑 → ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
65 61 63 64 3eqtr3d ⊢ ( 𝜑 → ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
66 eqid ⊢ ( *𝑟 ‘ 𝑅 ) = ( *𝑟 ‘ 𝑅 )
67 eqid ⊢ ( *rf ‘ 𝑅 ) = ( *rf ‘ 𝑅 )
68 10 66 67 stafval ⊢ ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) → ( ( *rf ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
69 32 68 syl ⊢ ( 𝜑 → ( ( *rf ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
70 65 69 33 3eqtr4d ⊢ ( 𝜑 → ( ( *rf ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
71 49 imp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
72 10 14 12 15 opprmul ⊢ ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ( .r ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) )
73 71 72 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
74 10 14 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
75 74 3expb ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
76 5 75 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
77 10 66 67 stafval ⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
78 76 77 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
79 10 66 67 stafval ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( ( *rf ‘ 𝑅 ) ‘ 𝑥 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) )
80 10 66 67 stafval ⊢ ( 𝑦 ∈ ( Base ‘ 𝑅 ) → ( ( *rf ‘ 𝑅 ) ‘ 𝑦 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) )
81 79 80 oveqan12d ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( *rf ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) ( ( *rf ‘ 𝑅 ) ‘ 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
82 81 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( *rf ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) ( ( *rf ‘ 𝑅 ) ‘ 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
83 73 78 82 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *rf ‘ 𝑅 ) ‘ 𝑥 ) ( .r ‘ ( oppr ‘ 𝑅 ) ) ( ( *rf ‘ 𝑅 ) ‘ 𝑦 ) ) )
84 12 10 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
85 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
86 12 85 oppradd ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( oppr ‘ 𝑅 ) )
87 38 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
88 10 66 67 staffval ⊢ ( *rf ‘ 𝑅 ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) )
89 87 88 fmptd ⊢ ( 𝜑 → ( *rf ‘ 𝑅 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
90 7 3expib ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( ∗ ‘ ( 𝑥 + 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) + ( ∗ ‘ 𝑦 ) ) ) )
91 2 oveqd ⊢ ( 𝜑 → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) )
92 4 91 fveq12d ⊢ ( 𝜑 → ( ∗ ‘ ( 𝑥 + 𝑦 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) )
93 2 24 46 oveq123d ⊢ ( 𝜑 → ( ( ∗ ‘ 𝑥 ) + ( ∗ ‘ 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
94 92 93 eqeq12d ⊢ ( 𝜑 → ( ( ∗ ‘ ( 𝑥 + 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) + ( ∗ ‘ 𝑦 ) ) ↔ ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) ) )
95 90 43 94 3imtr3d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) ) )
96 95 imp ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
97 10 85 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
98 97 3expb ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
99 5 98 sylan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
100 10 66 67 stafval ⊢ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) )
101 99 100 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) )
102 79 80 oveqan12d ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( *rf ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( *rf ‘ 𝑅 ) ‘ 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
103 102 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( ( *rf ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( *rf ‘ 𝑅 ) ‘ 𝑦 ) ) = ( ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
104 96 101 103 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( *rf ‘ 𝑅 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( ( *rf ‘ 𝑅 ) ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( ( *rf ‘ 𝑅 ) ‘ 𝑦 ) ) )
105 10 11 13 14 15 5 17 70 83 84 85 86 89 104 isrhmd ⊢ ( 𝜑 → ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) )
106 10 66 67 staffval ⊢ ( *rf ‘ 𝑅 ) = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) )
107 106 fmpt ⊢ ( ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) ↔ ( *rf ‘ 𝑅 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑅 ) )
108 89 107 sylibr ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
109 108 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
110 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
111 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) )
112 111 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
113 110 112 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) ↔ 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) ) )
114 113 rspccva ⊢ ( ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
115 30 114 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
116 115 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
117 fveq2 ⊢ ( 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) → ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
118 117 eqeq2d ⊢ ( 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) → ( 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ↔ 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) ) )
119 116 118 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) → 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
120 29 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
121 fveq2 ⊢ ( 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) → ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
122 121 eqeq2d ⊢ ( 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) → ( 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ↔ 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) ) )
123 120 122 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) → 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
124 119 123 impbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ↔ 𝑦 = ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑥 ) ) )
125 88 87 109 124 f1ocnv2d ⊢ ( 𝜑 → ( ( *rf ‘ 𝑅 ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑅 ) ∧ ◡ ( *rf ‘ 𝑅 ) = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) ) )
126 125 simprd ⊢ ( 𝜑 → ◡ ( *rf ‘ 𝑅 ) = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( *𝑟 ‘ 𝑅 ) ‘ 𝑦 ) ) )
127 106 126 eqtr4id ⊢ ( 𝜑 → ( *rf ‘ 𝑅 ) = ◡ ( *rf ‘ 𝑅 ) )
128 12 67 issrng ⊢ ( 𝑅 ∈ *-Ring ↔ ( ( *rf ‘ 𝑅 ) ∈ ( 𝑅 RingHom ( oppr ‘ 𝑅 ) ) ∧ ( *rf ‘ 𝑅 ) = ◡ ( *rf ‘ 𝑅 ) ) )
129 105 127 128 sylanbrc ⊢ ( 𝜑 → 𝑅 ∈ *-Ring )