Theorem rngurd

Description: Deduce the unit of a ring from its properties. (Contributed by Thierry Arnoux, 6-Sep-2016)

	Ref	Expression
Hypotheses	rngurd.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
	rngurd.p	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
	rngurd.z	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
	rngurd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
	rngurd.j	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{·}\underset{\dot{}}{1}=x$$
Assertion	rngurd	$$⊢\phi \to \underset{\dot{}}{1}=1_R$$

Proof

Step	Hyp	Ref	Expression
1		rngurd.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
2		rngurd.p	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_R$$
3		rngurd.z	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
4		rngurd.i	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
5		rngurd.j	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{·}\underset{\dot{}}{1}=x$$
6		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
7		eqid	$$⊢{\cdot }_R={\cdot }_R$$
8		eqid	$$⊢1_R=1_R$$
9	6 7 8	dfur2	$$⊢1_R=\left(\iota e|\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\right)$$
10	3 1	eleqtrd	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
11	4 5	jca	$$⊢\left(\phi \wedge x\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}\underset{\dot{}}{1}=x\right)$$
12	11	ralrimiva	$$⊢\phi \to \forall x\in B\left(\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}\underset{\dot{}}{1}=x\right)$$
13	2	adantr	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{·}={\cdot }_R$$
14	13	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=\underset{\dot{}}{1}{\cdot }_{R}x$$
15	14	eqeq1d	$$⊢\left(\phi \wedge x\in B\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\leftrightarrow \underset{\dot{}}{1}{\cdot }_{R}x=x\right)$$
16	13	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{·}\underset{\dot{}}{1}=x{\cdot }_R\underset{\dot{}}{1}$$
17	16	eqeq1d	$$⊢\left(\phi \wedge x\in B\right)\to \left(x\underset{\dot{}}{·}\underset{\dot{}}{1}=x\leftrightarrow x{\cdot }_R\underset{\dot{}}{1}=x\right)$$
18	15 17	anbi12d	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}\underset{\dot{}}{1}=x\right)\leftrightarrow \left(\underset{\dot{}}{1}{\cdot }_{R}x=x\wedge x{\cdot }_R\underset{\dot{}}{1}=x\right)\right)$$
19	1 18	raleqbidva	$$⊢\phi \to \left(\forall x\in B\left(\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}\underset{\dot{}}{1}=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_R\left(\underset{\dot{}}{1}{\cdot }_{R}x=x\wedge x{\cdot }_R\underset{\dot{}}{1}=x\right)\right)$$
20	12 19	mpbid	$$⊢\phi \to \forall x\in {\mathrm{Base}}_R\left(\underset{\dot{}}{1}{\cdot }_{R}x=x\wedge x{\cdot }_R\underset{\dot{}}{1}=x\right)$$
21	1	eleq2d	$$⊢\phi \to \left(e\in B\leftrightarrow e\in {\mathrm{Base}}_R\right)$$
22	13	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to e\underset{\dot{}}{·}x=e{\cdot }_{R}x$$
23	22	eqeq1d	$$⊢\left(\phi \wedge x\in B\right)\to \left(e\underset{\dot{}}{·}x=x\leftrightarrow e{\cdot }_{R}x=x\right)$$
24	13	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to x\underset{\dot{}}{·}e=x{\cdot }_{R}e$$
25	24	eqeq1d	$$⊢\left(\phi \wedge x\in B\right)\to \left(x\underset{\dot{}}{·}e=x\leftrightarrow x{\cdot }_{R}e=x\right)$$
26	23 25	anbi12d	$$⊢\left(\phi \wedge x\in B\right)\to \left(\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\leftrightarrow \left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)$$
27	1 26	raleqbidva	$$⊢\phi \to \left(\forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)$$
28	21 27	anbi12d	$$⊢\phi \to \left(\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\right)\leftrightarrow \left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\right)$$
29	4	ralrimiva	$$⊢\phi \to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
30	29	adantr	$$⊢\left(\phi \wedge e\in B\right)\to \forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
31		simpr	$$⊢\left(\phi \wedge e\in B\right)\to e\in B$$
32		simpr	$$⊢\left(\left(\phi \wedge e\in B\right)\wedge x=e\right)\to x=e$$
33	32	oveq2d	$$⊢\left(\left(\phi \wedge e\in B\right)\wedge x=e\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=\underset{\dot{}}{1}\underset{\dot{}}{·}e$$
34	33 32	eqeq12d	$$⊢\left(\left(\phi \wedge e\in B\right)\wedge x=e\right)\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{·}e=e\right)$$
35	31 34	rspcdv	$$⊢\left(\phi \wedge e\in B\right)\to \left(\forall x\in B\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\to \underset{\dot{}}{1}\underset{\dot{}}{·}e=e\right)$$
36	30 35	mpd	$$⊢\left(\phi \wedge e\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}e=e$$
37	36	adantrr	$$⊢\left(\phi \wedge \left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}e=e$$
38	3	adantr	$$⊢\left(\phi \wedge \left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\right)\right)\to \underset{\dot{}}{1}\in B$$
39		simprr	$$⊢\left(\phi \wedge \left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\right)\right)\to \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)$$
40		oveq2	$$⊢x=\underset{\dot{}}{1}\to e\underset{\dot{}}{·}x=e\underset{\dot{}}{·}\underset{\dot{}}{1}$$
41		id	$$⊢x=\underset{\dot{}}{1}\to x=\underset{\dot{}}{1}$$
42	40 41	eqeq12d	$$⊢x=\underset{\dot{}}{1}\to \left(e\underset{\dot{}}{·}x=x\leftrightarrow e\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}\right)$$
43		oveq1	$$⊢x=\underset{\dot{}}{1}\to x\underset{\dot{}}{·}e=\underset{\dot{}}{1}\underset{\dot{}}{·}e$$
44	43 41	eqeq12d	$$⊢x=\underset{\dot{}}{1}\to \left(x\underset{\dot{}}{·}e=x\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{·}e=\underset{\dot{}}{1}\right)$$
45	42 44	anbi12d	$$⊢x=\underset{\dot{}}{1}\to \left(\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\leftrightarrow \left(e\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}e=\underset{\dot{}}{1}\right)\right)$$
46	45	rspcva	$$⊢\left(\underset{\dot{}}{1}\in B\wedge \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\right)\to \left(e\underset{\dot{}}{·}\underset{\dot{}}{1}=\underset{\dot{}}{1}\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}e=\underset{\dot{}}{1}\right)$$
47	46	simprd	$$⊢\left(\underset{\dot{}}{1}\in B\wedge \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}e=\underset{\dot{}}{1}$$
48	38 39 47	syl2anc	$$⊢\left(\phi \wedge \left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}e=\underset{\dot{}}{1}$$
49	37 48	eqtr3d	$$⊢\left(\phi \wedge \left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\right)\right)\to e=\underset{\dot{}}{1}$$
50	49	ex	$$⊢\phi \to \left(\left(e\in B\wedge \forall x\in B\left(e\underset{\dot{}}{·}x=x\wedge x\underset{\dot{}}{·}e=x\right)\right)\to e=\underset{\dot{}}{1}\right)$$
51	28 50	sylbird	$$⊢\phi \to \left(\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\to e=\underset{\dot{}}{1}\right)$$
52	51	alrimiv	$$⊢\phi \to \forall e\left(\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\to e=\underset{\dot{}}{1}\right)$$
53		eleq1	$$⊢e=\underset{\dot{}}{1}\to \left(e\in {\mathrm{Base}}_R\leftrightarrow \underset{\dot{}}{1}\in {\mathrm{Base}}_R\right)$$
54		oveq1	$$⊢e=\underset{\dot{}}{1}\to e{\cdot }_{R}x=\underset{\dot{}}{1}{\cdot }_{R}x$$
55	54	eqeq1d	$$⊢e=\underset{\dot{}}{1}\to \left(e{\cdot }_{R}x=x\leftrightarrow \underset{\dot{}}{1}{\cdot }_{R}x=x\right)$$
56	55	ovanraleqv	$$⊢e=\underset{\dot{}}{1}\to \left(\forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\leftrightarrow \forall x\in {\mathrm{Base}}_R\left(\underset{\dot{}}{1}{\cdot }_{R}x=x\wedge x{\cdot }_R\underset{\dot{}}{1}=x\right)\right)$$
57	53 56	anbi12d	$$⊢e=\underset{\dot{}}{1}\to \left(\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\leftrightarrow \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(\underset{\dot{}}{1}{\cdot }_{R}x=x\wedge x{\cdot }_R\underset{\dot{}}{1}=x\right)\right)\right)$$
58	57	eqeu	$$⊢\left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(\underset{\dot{}}{1}{\cdot }_{R}x=x\wedge x{\cdot }_R\underset{\dot{}}{1}=x\right)\right)\wedge \forall e\left(\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\to e=\underset{\dot{}}{1}\right)\right)\to \exists !e\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)$$
59	10 10 20 52 58	syl121anc	$$⊢\phi \to \exists !e\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)$$
60	57	iota2	$$⊢\left(\underset{\dot{}}{1}\in B\wedge \exists !e\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\right)\to \left(\left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(\underset{\dot{}}{1}{\cdot }_{R}x=x\wedge x{\cdot }_R\underset{\dot{}}{1}=x\right)\right)\leftrightarrow \left(\iota e|\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\right)=\underset{\dot{}}{1}\right)$$
61	3 59 60	syl2anc	$$⊢\phi \to \left(\left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(\underset{\dot{}}{1}{\cdot }_{R}x=x\wedge x{\cdot }_R\underset{\dot{}}{1}=x\right)\right)\leftrightarrow \left(\iota e|\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\right)=\underset{\dot{}}{1}\right)$$
62	10 20 61	mpbi2and	$$⊢\phi \to \left(\iota e|\left(e\in {\mathrm{Base}}_R\wedge \forall x\in {\mathrm{Base}}_R\left(e{\cdot }_{R}x=x\wedge x{\cdot }_{R}e=x\right)\right)\right)=\underset{\dot{}}{1}$$
63	9 62	syl5req	$$⊢\phi \to \underset{\dot{}}{1}=1_R$$