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	$⊢ φ \to B = {Base}_{R}$
	isdrngdOLD.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
	isdrngdOLD.z	$⊢ φ \to \underset{˙}{0} = 0_{R}$
	isdrngdOLD.u	$⊢ φ \to \underset{˙}{1} = 1_{R}$
	isdrngdOLD.r	$⊢ φ \to R \in Ring$
	isdrngdOLD.n	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} y \neq \underset{˙}{0}$
	isdrngdOLD.o	$⊢ φ \to \underset{˙}{1} \neq \underset{˙}{0}$
	isdrngdOLD.i	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \in B$
	isdrngdOLD.j	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \neq \underset{˙}{0}$
	isdrngrdOLD.k	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} I = \underset{˙}{1}$
Assertion	isdrngrdOLD	$⊢ φ \to R \in DivRing$

Proof

Step	Hyp	Ref	Expression
1		isdrngdOLD.b	$⊢ φ \to B = {Base}_{R}$
2		isdrngdOLD.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
3		isdrngdOLD.z	$⊢ φ \to \underset{˙}{0} = 0_{R}$
4		isdrngdOLD.u	$⊢ φ \to \underset{˙}{1} = 1_{R}$
5		isdrngdOLD.r	$⊢ φ \to R \in Ring$
6		isdrngdOLD.n	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} y \neq \underset{˙}{0}$
7		isdrngdOLD.o	$⊢ φ \to \underset{˙}{1} \neq \underset{˙}{0}$
8		isdrngdOLD.i	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \in B$
9		isdrngdOLD.j	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \neq \underset{˙}{0}$
10		isdrngrdOLD.k	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} I = \underset{˙}{1}$
11		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13	11 12	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (R)}$
14	1 13	eqtrdi	$⊢ φ \to B = {Base}_{{opp}_{r} (R)}$
15		eqidd	$⊢ φ \to \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
16		eqid	$⊢ 0_{R} = 0_{R}$
17	11 16	oppr0	$⊢ 0_{R} = 0_{{opp}_{r} (R)}$
18	3 17	eqtrdi	$⊢ φ \to \underset{˙}{0} = 0_{{opp}_{r} (R)}$
19		eqid	$⊢ 1_{R} = 1_{R}$
20	11 19	oppr1	$⊢ 1_{R} = 1_{{opp}_{r} (R)}$
21	4 20	eqtrdi	$⊢ φ \to \underset{˙}{1} = 1_{{opp}_{r} (R)}$
22	11	opprring	$⊢ R \in Ring \to {opp}_{r} (R) \in Ring$
23	5 22	syl	$⊢ φ \to {opp}_{r} (R) \in Ring$
24		eleq1w	$⊢ y = x \to (y \in B \leftrightarrow x \in B)$
25		neeq1	$⊢ y = x \to (y \neq \underset{˙}{0} \leftrightarrow x \neq \underset{˙}{0})$
26	24 25	anbi12d	$⊢ y = x \to ((y \in B \land y \neq \underset{˙}{0}) \leftrightarrow (x \in B \land x \neq \underset{˙}{0}))$
27	26	3anbi2d	$⊢ y = x \to ((φ \land (y \in B \land y \neq \underset{˙}{0}) \land (z \in B \land z \neq \underset{˙}{0})) \leftrightarrow (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (z \in B \land z \neq \underset{˙}{0})))$
28		oveq1	$⊢ y = x \to y \cdot_{{opp}_{r} (R)} z = x \cdot_{{opp}_{r} (R)} z$
29	28	neeq1d	$⊢ y = x \to (y \cdot_{{opp}_{r} (R)} z \neq \underset{˙}{0} \leftrightarrow x \cdot_{{opp}_{r} (R)} z \neq \underset{˙}{0})$
30	27 29	imbi12d	$⊢ y = x \to (((φ \land (y \in B \land y \neq \underset{˙}{0}) \land (z \in B \land z \neq \underset{˙}{0})) \to y \cdot_{{opp}_{r} (R)} z \neq \underset{˙}{0}) \leftrightarrow ((φ \land (x \in B \land x \neq \underset{˙}{0}) \land (z \in B \land z \neq \underset{˙}{0})) \to x \cdot_{{opp}_{r} (R)} z \neq \underset{˙}{0}))$
31		eleq1w	$⊢ x = z \to (x \in B \leftrightarrow z \in B)$
32		neeq1	$⊢ x = z \to (x \neq \underset{˙}{0} \leftrightarrow z \neq \underset{˙}{0})$
33	31 32	anbi12d	$⊢ x = z \to ((x \in B \land x \neq \underset{˙}{0}) \leftrightarrow (z \in B \land z \neq \underset{˙}{0}))$
34	33	3anbi3d	$⊢ x = z \to ((φ \land (y \in B \land y \neq \underset{˙}{0}) \land (x \in B \land x \neq \underset{˙}{0})) \leftrightarrow (φ \land (y \in B \land y \neq \underset{˙}{0}) \land (z \in B \land z \neq \underset{˙}{0})))$
35		oveq2	$⊢ x = z \to y \cdot_{{opp}_{r} (R)} x = y \cdot_{{opp}_{r} (R)} z$
36	35	neeq1d	$⊢ x = z \to (y \cdot_{{opp}_{r} (R)} x \neq \underset{˙}{0} \leftrightarrow y \cdot_{{opp}_{r} (R)} z \neq \underset{˙}{0})$
37	34 36	imbi12d	$⊢ x = z \to (((φ \land (y \in B \land y \neq \underset{˙}{0}) \land (x \in B \land x \neq \underset{˙}{0})) \to y \cdot_{{opp}_{r} (R)} x \neq \underset{˙}{0}) \leftrightarrow ((φ \land (y \in B \land y \neq \underset{˙}{0}) \land (z \in B \land z \neq \underset{˙}{0})) \to y \cdot_{{opp}_{r} (R)} z \neq \underset{˙}{0}))$
38	2	3ad2ant1	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to \underset{˙}{\cdot} = \cdot_{R}$
39	38	oveqd	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} y = x \cdot_{R} y$
40		eqid	$⊢ \cdot_{R} = \cdot_{R}$
41		eqid	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
42	12 40 11 41	opprmul	$⊢ y \cdot_{{opp}_{r} (R)} x = x \cdot_{R} y$
43	39 42	eqtr4di	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} y = y \cdot_{{opp}_{r} (R)} x$
44	43 6	eqnetrrd	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (y \in B \land y \neq \underset{˙}{0})) \to y \cdot_{{opp}_{r} (R)} x \neq \underset{˙}{0}$
45	44	3com23	$⊢ (φ \land (y \in B \land y \neq \underset{˙}{0}) \land (x \in B \land x \neq \underset{˙}{0})) \to y \cdot_{{opp}_{r} (R)} x \neq \underset{˙}{0}$
46	37 45	chvarvv	$⊢ (φ \land (y \in B \land y \neq \underset{˙}{0}) \land (z \in B \land z \neq \underset{˙}{0})) \to y \cdot_{{opp}_{r} (R)} z \neq \underset{˙}{0}$
47	30 46	chvarvv	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0}) \land (z \in B \land z \neq \underset{˙}{0})) \to x \cdot_{{opp}_{r} (R)} z \neq \underset{˙}{0}$
48	12 40 11 41	opprmul	$⊢ I \cdot_{{opp}_{r} (R)} x = x \cdot_{R} I$
49	2	adantr	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to \underset{˙}{\cdot} = \cdot_{R}$
50	49	oveqd	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to x \underset{˙}{\cdot} I = x \cdot_{R} I$
51	50 10	eqtr3d	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to x \cdot_{R} I = \underset{˙}{1}$
52	48 51	eqtrid	$⊢ (φ \land (x \in B \land x \neq \underset{˙}{0})) \to I \cdot_{{opp}_{r} (R)} x = \underset{˙}{1}$
53	14 15 18 21 23 47 7 8 9 52	isdrngdOLD	$⊢ φ \to {opp}_{r} (R) \in DivRing$
54	11	opprdrng	$⊢ R \in DivRing \leftrightarrow {opp}_{r} (R) \in DivRing$
55	53 54	sylibr	$⊢ φ \to R \in DivRing$

Metamath Proof Explorer

Theorem isdrngrdOLD

Proof