Theorem oppr1

Description: Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

	Ref	Expression
Hypotheses	opprbas.1	$$⊢O={opp}_r\left(R\right)$$
	oppr1.2	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	oppr1	$$⊢\underset{\dot{}}{1}=1_O$$

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	$$⊢O={opp}_r\left(R\right)$$
2		oppr1.2	$$⊢\underset{\dot{}}{1}=1_R$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4		eqid	$$⊢{\cdot }_R={\cdot }_R$$
5		eqid	$$⊢{\cdot }_O={\cdot }_O$$
6	3 4 1 5	opprmul	$$⊢x{\cdot }_{O}y=y{\cdot }_{R}x$$
7	6	eqeq1i	$$⊢x{\cdot }_{O}y=y\leftrightarrow y{\cdot }_{R}x=y$$
8	3 4 1 5	opprmul	$$⊢y{\cdot }_{O}x=x{\cdot }_{R}y$$
9	8	eqeq1i	$$⊢y{\cdot }_{O}x=y\leftrightarrow x{\cdot }_{R}y=y$$
10	7 9	anbi12ci	$$⊢\left(x{\cdot }_{O}y=y\wedge y{\cdot }_{O}x=y\right)\leftrightarrow \left(x{\cdot }_{R}y=y\wedge y{\cdot }_{R}x=y\right)$$
11	10	ralbii	$$⊢\forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{O}y=y\wedge y{\cdot }_{O}x=y\right)\leftrightarrow \forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{R}y=y\wedge y{\cdot }_{R}x=y\right)$$
12	11	anbi2i	$$⊢\left(x\in {\mathrm{Base}}_R\wedge \forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{O}y=y\wedge y{\cdot }_{O}x=y\right)\right)\leftrightarrow \left(x\in {\mathrm{Base}}_R\wedge \forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{R}y=y\wedge y{\cdot }_{R}x=y\right)\right)$$
13	12	iotabii	$$⊢\left(\iota x|\left(x\in {\mathrm{Base}}_R\wedge \forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{O}y=y\wedge y{\cdot }_{O}x=y\right)\right)\right)=\left(\iota x|\left(x\in {\mathrm{Base}}_R\wedge \forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{R}y=y\wedge y{\cdot }_{R}x=y\right)\right)\right)$$
14		eqid	$$⊢{\mathrm{mulGrp}}_O={\mathrm{mulGrp}}_O$$
15	1 3	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
16	14 15	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_O}$$
17	14 5	mgpplusg	$$⊢{\cdot }_O={+}_{{\mathrm{mulGrp}}_O}$$
18		eqid	$$⊢0_{{\mathrm{mulGrp}}_O}=0_{{\mathrm{mulGrp}}_O}$$
19	16 17 18	grpidval	$$⊢0_{{\mathrm{mulGrp}}_O}=\left(\iota x|\left(x\in {\mathrm{Base}}_R\wedge \forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{O}y=y\wedge y{\cdot }_{O}x=y\right)\right)\right)$$
20		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
21	20 3	mgpbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{\mathrm{mulGrp}}_R}$$
22	20 4	mgpplusg	$$⊢{\cdot }_R={+}_{{\mathrm{mulGrp}}_R}$$
23		eqid	$$⊢0_{{\mathrm{mulGrp}}_R}=0_{{\mathrm{mulGrp}}_R}$$
24	21 22 23	grpidval	$$⊢0_{{\mathrm{mulGrp}}_R}=\left(\iota x|\left(x\in {\mathrm{Base}}_R\wedge \forall y\in {\mathrm{Base}}_R\left(x{\cdot }_{R}y=y\wedge y{\cdot }_{R}x=y\right)\right)\right)$$
25	13 19 24	3eqtr4i	$$⊢0_{{\mathrm{mulGrp}}_O}=0_{{\mathrm{mulGrp}}_R}$$
26		eqid	$$⊢1_O=1_O$$
27	14 26	ringidval	$$⊢1_O=0_{{\mathrm{mulGrp}}_O}$$
28	20 2	ringidval	$$⊢\underset{\dot{}}{1}=0_{{\mathrm{mulGrp}}_R}$$
29	25 27 28	3eqtr4ri	$$⊢\underset{\dot{}}{1}=1_O$$