# Metamath Proof Explorer

## 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
Assertion oppr1

### Proof

Step Hyp Ref Expression
1 opprbas.1 ${⊢}{O}={opp}_{r}\left({R}\right)$
2 oppr1.2
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}↔{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}↔{x}{\cdot }_{{R}}{y}={y}$
10 7 9 anbi12ci ${⊢}\left({x}{\cdot }_{{O}}{y}={y}\wedge {y}{\cdot }_{{O}}{x}={y}\right)↔\left({x}{\cdot }_{{R}}{y}={y}\wedge {y}{\cdot }_{{R}}{x}={y}\right)$
11 10 ralbii ${⊢}\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{O}}{y}={y}\wedge {y}{\cdot }_{{O}}{x}={y}\right)↔\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{O}}{y}={y}\wedge {y}{\cdot }_{{O}}{x}={y}\right)\right)↔\left({x}\in {\mathrm{Base}}_{{R}}\wedge \forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\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
29 25 27 28 3eqtr4ri