# Metamath Proof Explorer

## Theorem opprsubg

Description: Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014)

Ref Expression
Hypothesis opprbas.1 ${⊢}{O}={opp}_{r}\left({R}\right)$
Assertion opprsubg ${⊢}\mathrm{SubGrp}\left({R}\right)=\mathrm{SubGrp}\left({O}\right)$

### Proof

Step Hyp Ref Expression
1 opprbas.1 ${⊢}{O}={opp}_{r}\left({R}\right)$
2 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
3 1 2 opprbas ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{O}}$
4 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
5 1 4 oppradd ${⊢}{+}_{{R}}={+}_{{O}}$
6 3 5 grpprop ${⊢}{R}\in \mathrm{Grp}↔{O}\in \mathrm{Grp}$
7 biid ${⊢}{x}\subseteq {\mathrm{Base}}_{{R}}↔{x}\subseteq {\mathrm{Base}}_{{R}}$
8 eqid ${⊢}{R}{↾}_{𝑠}{x}={R}{↾}_{𝑠}{x}$
9 8 2 ressbas ${⊢}{x}\in \mathrm{V}\to {x}\cap {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\left({R}{↾}_{𝑠}{x}\right)}$
10 9 elv ${⊢}{x}\cap {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\left({R}{↾}_{𝑠}{x}\right)}$
11 eqid ${⊢}{O}{↾}_{𝑠}{x}={O}{↾}_{𝑠}{x}$
12 11 3 ressbas ${⊢}{x}\in \mathrm{V}\to {x}\cap {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\left({O}{↾}_{𝑠}{x}\right)}$
13 12 elv ${⊢}{x}\cap {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\left({O}{↾}_{𝑠}{x}\right)}$
14 10 13 eqtr3i ${⊢}{\mathrm{Base}}_{\left({R}{↾}_{𝑠}{x}\right)}={\mathrm{Base}}_{\left({O}{↾}_{𝑠}{x}\right)}$
15 8 4 ressplusg ${⊢}{x}\in \mathrm{V}\to {+}_{{R}}={+}_{\left({R}{↾}_{𝑠}{x}\right)}$
16 11 5 ressplusg ${⊢}{x}\in \mathrm{V}\to {+}_{{R}}={+}_{\left({O}{↾}_{𝑠}{x}\right)}$
17 15 16 eqtr3d ${⊢}{x}\in \mathrm{V}\to {+}_{\left({R}{↾}_{𝑠}{x}\right)}={+}_{\left({O}{↾}_{𝑠}{x}\right)}$
18 17 elv ${⊢}{+}_{\left({R}{↾}_{𝑠}{x}\right)}={+}_{\left({O}{↾}_{𝑠}{x}\right)}$
19 14 18 grpprop ${⊢}{R}{↾}_{𝑠}{x}\in \mathrm{Grp}↔{O}{↾}_{𝑠}{x}\in \mathrm{Grp}$
20 6 7 19 3anbi123i ${⊢}\left({R}\in \mathrm{Grp}\wedge {x}\subseteq {\mathrm{Base}}_{{R}}\wedge {R}{↾}_{𝑠}{x}\in \mathrm{Grp}\right)↔\left({O}\in \mathrm{Grp}\wedge {x}\subseteq {\mathrm{Base}}_{{R}}\wedge {O}{↾}_{𝑠}{x}\in \mathrm{Grp}\right)$
21 2 issubg ${⊢}{x}\in \mathrm{SubGrp}\left({R}\right)↔\left({R}\in \mathrm{Grp}\wedge {x}\subseteq {\mathrm{Base}}_{{R}}\wedge {R}{↾}_{𝑠}{x}\in \mathrm{Grp}\right)$
22 3 issubg ${⊢}{x}\in \mathrm{SubGrp}\left({O}\right)↔\left({O}\in \mathrm{Grp}\wedge {x}\subseteq {\mathrm{Base}}_{{R}}\wedge {O}{↾}_{𝑠}{x}\in \mathrm{Grp}\right)$
23 20 21 22 3bitr4i ${⊢}{x}\in \mathrm{SubGrp}\left({R}\right)↔{x}\in \mathrm{SubGrp}\left({O}\right)$
24 23 eqriv ${⊢}\mathrm{SubGrp}\left({R}\right)=\mathrm{SubGrp}\left({O}\right)$