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 )