Theorem isdrngrdOLD

Description: Obsolete version of isdrngrd as of 19-Feb-2025. (Contributed by NM, 10-Aug-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isdrngdOLD.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
	isdrngdOLD.t	⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
	isdrngdOLD.z	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
	isdrngdOLD.u	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑅 ) )
	isdrngdOLD.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	isdrngdOLD.n	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
	isdrngdOLD.o	⊢ ( 𝜑 → 1 ≠ 0 )
	isdrngdOLD.i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ 𝐵 )
	isdrngdOLD.j	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ≠ 0 )
	isdrngrdOLD.k	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 · 𝐼 ) = 1 )
Assertion	isdrngrdOLD	⊢ ( 𝜑 → 𝑅 ∈ DivRing )

Proof

Step	Hyp	Ref	Expression
1		isdrngdOLD.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
2		isdrngdOLD.t	⊢ ( 𝜑 → · = ( .r ‘ 𝑅 ) )
3		isdrngdOLD.z	⊢ ( 𝜑 → 0 = ( 0g ‘ 𝑅 ) )
4		isdrngdOLD.u	⊢ ( 𝜑 → 1 = ( 1r ‘ 𝑅 ) )
5		isdrngdOLD.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		isdrngdOLD.n	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
7		isdrngdOLD.o	⊢ ( 𝜑 → 1 ≠ 0 )
8		isdrngdOLD.i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ 𝐵 )
9		isdrngdOLD.j	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ≠ 0 )
10		isdrngrdOLD.k	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 · 𝐼 ) = 1 )
11		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
12		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13	11 12	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
14	1 13	eqtrdi	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) ) )
15		eqidd	⊢ ( 𝜑 → ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) ) )
16		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
17	11 16	oppr0	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ ( oppr ‘ 𝑅 ) )
18	3 17	eqtrdi	⊢ ( 𝜑 → 0 = ( 0g ‘ ( oppr ‘ 𝑅 ) ) )
19		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20	11 19	oppr1	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ ( oppr ‘ 𝑅 ) )
21	4 20	eqtrdi	⊢ ( 𝜑 → 1 = ( 1r ‘ ( oppr ‘ 𝑅 ) ) )
22	11	opprring	⊢ ( 𝑅 ∈ Ring → ( oppr ‘ 𝑅 ) ∈ Ring )
23	5 22	syl	⊢ ( 𝜑 → ( oppr ‘ 𝑅 ) ∈ Ring )
24		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
25		neeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≠ 0 ↔ 𝑥 ≠ 0 ) )
26	24 25	anbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) )
27	26	3anbi2d	⊢ ( 𝑦 = 𝑥 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ↔ ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ) )
28		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) = ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) )
29	28	neeq1d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ↔ ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) )
30	27 29	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ) )
31		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
32		neeq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≠ 0 ↔ 𝑧 ≠ 0 ) )
33	31 32	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ↔ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) )
34	33	3anbi3d	⊢ ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) ↔ ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) ) )
35		oveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) )
36	35	neeq1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 ↔ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) )
37	34 36	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 ) ) )
38	2	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → · = ( .r ‘ 𝑅 ) )
39	38	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
40		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
41		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
42	12 40 11 41	opprmul	⊢ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 )
43	39 42	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) )
44	43 6	eqnetrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 )
45	44	3com23	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) ≠ 0 )
46	37 45	chvarvv	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 )
47	30 46	chvarvv	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑧 ≠ 0 ) ) → ( 𝑥 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑧 ) ≠ 0 )
48	12 40 11 41	opprmul	⊢ ( 𝐼 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝐼 )
49	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → · = ( .r ‘ 𝑅 ) )
50	49	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 · 𝐼 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝐼 ) )
51	50 10	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝐼 ) = 1 )
52	48 51	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝐼 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = 1 )
53	14 15 18 21 23 47 7 8 9 52	isdrngdOLD	⊢ ( 𝜑 → ( oppr ‘ 𝑅 ) ∈ DivRing )
54	11	opprdrng	⊢ ( 𝑅 ∈ DivRing ↔ ( oppr ‘ 𝑅 ) ∈ DivRing )
55	53 54	sylibr	⊢ ( 𝜑 → 𝑅 ∈ DivRing )