Theorem isdrngdOLD

Description: Obsolete version of isdrngd as of 19-Feb-2025. (Contributed by NM, 2-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 )
	isdrngdOLD.k	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝐼 · 𝑥 ) = 1 )
Assertion	isdrngdOLD	⊢ ( 𝜑 → 𝑅 ∈ 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		isdrngdOLD.k	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝐼 · 𝑥 ) = 1 )
11		difss	⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
12	11 1	sseqtrid	⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) ⊆ ( Base ‘ 𝑅 ) )
13		eqid	⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
14		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
15		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16	14 15	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
17	13 16	ressbas2	⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ ( Base ‘ 𝑅 ) → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
18	12 17	syl	⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
19		fvex	⊢ ( Base ‘ 𝑅 ) ∈ V
20	1 19	eqeltrdi	⊢ ( 𝜑 → 𝐵 ∈ V )
21		difexg	⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { 0 } ) ∈ V )
22		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
23	14 22	mgpplusg	⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
24	13 23	ressplusg	⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → ( .r ‘ 𝑅 ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
25	20 21 24	3syl	⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
26	2 25	eqtrd	⊢ ( 𝜑 → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
27		eldifsn	⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) )
28		eldifsn	⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) )
29	15 22	ringcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
30	5 29	syl3an1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
31	30	3expib	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
32	1	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
33	1	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
34	32 33	anbi12d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) )
35	2	oveqd	⊢ ( 𝜑 → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
36	35 1	eleq12d	⊢ ( 𝜑 → ( ( 𝑥 · 𝑦 ) ∈ 𝐵 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
37	31 34 36	3imtr4d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 ) )
38	37	3impib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
39	38	3adant2r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
40	39	3adant3r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
41		eldifsn	⊢ ( ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ 𝐵 ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
42	40 6 41	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
43	28 42	syl3an3b	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
44	27 43	syl3an2b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
45	15 22	ringass	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
46	45	ex	⊢ ( 𝑅 ∈ Ring → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) )
47	5 46	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) )
48	1	eleq2d	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ ( Base ‘ 𝑅 ) ) )
49	32 33 48	3anbi123d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) )
50		eqidd	⊢ ( 𝜑 → 𝑧 = 𝑧 )
51	2 35 50	oveq123d	⊢ ( 𝜑 → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) )
52		eqidd	⊢ ( 𝜑 → 𝑥 = 𝑥 )
53	2	oveqd	⊢ ( 𝜑 → ( 𝑦 · 𝑧 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) )
54	2 52 53	oveq123d	⊢ ( 𝜑 → ( 𝑥 · ( 𝑦 · 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
55	51 54	eqeq12d	⊢ ( 𝜑 → ( ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) )
56	47 49 55	3imtr4d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) )
57		eldifi	⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ∈ 𝐵 )
58		eldifi	⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → 𝑦 ∈ 𝐵 )
59		eldifi	⊢ ( 𝑧 ∈ ( 𝐵 ∖ { 0 } ) → 𝑧 ∈ 𝐵 )
60	57 58 59	3anim123i	⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑧 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) )
61	56 60	impel	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑧 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
62		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
63	15 62	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
64	5 63	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
65	64 4 1	3eltr4d	⊢ ( 𝜑 → 1 ∈ 𝐵 )
66		eldifsn	⊢ ( 1 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 1 ∈ 𝐵 ∧ 1 ≠ 0 ) )
67	65 7 66	sylanbrc	⊢ ( 𝜑 → 1 ∈ ( 𝐵 ∖ { 0 } ) )
68	15 22 62	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
69	68	ex	⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
70	5 69	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
71	2 4 52	oveq123d	⊢ ( 𝜑 → ( 1 · 𝑥 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) )
72	71	eqeq1d	⊢ ( 𝜑 → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
73	70 32 72	3imtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( 1 · 𝑥 ) = 𝑥 ) )
74	73	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
75	74	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 1 · 𝑥 ) = 𝑥 )
76	27 75	sylan2b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 1 · 𝑥 ) = 𝑥 )
77		eldifsn	⊢ ( 𝐼 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ) )
78	8 9 77	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ ( 𝐵 ∖ { 0 } ) )
79	27 78	sylan2b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝐼 ∈ ( 𝐵 ∖ { 0 } ) )
80	27 10	sylan2b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝐼 · 𝑥 ) = 1 )
81	18 26 44 61 67 76 79 80	isgrpd	⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp )
82	3	sneqd	⊢ ( 𝜑 → { 0 } = { ( 0g ‘ 𝑅 ) } )
83	1 82	difeq12d	⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
84	83	oveq2d	⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) )
85	84	eleq1d	⊢ ( 𝜑 → ( ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ↔ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) )
86	85	anbi2d	⊢ ( 𝜑 → ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ↔ ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) ) )
87	5 81 86	mpbi2and	⊢ ( 𝜑 → ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) )
88		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
89		eqid	⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
90	15 88 89	isdrng2	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) )
91	87 90	sylibr	⊢ ( 𝜑 → 𝑅 ∈ DivRing )