# Metamath Proof Explorer

## Theorem oppgsubm

Description: Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015)

Ref Expression
Hypothesis oppggic.o $⊢ O = opp 𝑔 ⁡ G$
Assertion oppgsubm $⊢ SubMnd ⁡ G = SubMnd ⁡ O$

### Proof

Step Hyp Ref Expression
1 oppggic.o $⊢ O = opp 𝑔 ⁡ G$
2 submrcl $⊢ x ∈ SubMnd ⁡ G → G ∈ Mnd$
3 submrcl $⊢ x ∈ SubMnd ⁡ O → O ∈ Mnd$
4 1 oppgmndb $⊢ G ∈ Mnd ↔ O ∈ Mnd$
5 3 4 sylibr $⊢ x ∈ SubMnd ⁡ O → G ∈ Mnd$
6 ralcom $⊢ ∀ y ∈ x ∀ z ∈ x y + G z ∈ x ↔ ∀ z ∈ x ∀ y ∈ x y + G z ∈ x$
7 eqid $⊢ + G = + G$
8 eqid $⊢ + O = + O$
9 7 1 8 oppgplus $⊢ z + O y = y + G z$
10 9 eleq1i $⊢ z + O y ∈ x ↔ y + G z ∈ x$
11 10 2ralbii $⊢ ∀ z ∈ x ∀ y ∈ x z + O y ∈ x ↔ ∀ z ∈ x ∀ y ∈ x y + G z ∈ x$
12 6 11 bitr4i $⊢ ∀ y ∈ x ∀ z ∈ x y + G z ∈ x ↔ ∀ z ∈ x ∀ y ∈ x z + O y ∈ x$
13 12 3anbi3i $⊢ x ⊆ Base G ∧ 0 G ∈ x ∧ ∀ y ∈ x ∀ z ∈ x y + G z ∈ x ↔ x ⊆ Base G ∧ 0 G ∈ x ∧ ∀ z ∈ x ∀ y ∈ x z + O y ∈ x$
14 13 a1i $⊢ G ∈ Mnd → x ⊆ Base G ∧ 0 G ∈ x ∧ ∀ y ∈ x ∀ z ∈ x y + G z ∈ x ↔ x ⊆ Base G ∧ 0 G ∈ x ∧ ∀ z ∈ x ∀ y ∈ x z + O y ∈ x$
15 eqid $⊢ Base G = Base G$
16 eqid $⊢ 0 G = 0 G$
17 15 16 7 issubm $⊢ G ∈ Mnd → x ∈ SubMnd ⁡ G ↔ x ⊆ Base G ∧ 0 G ∈ x ∧ ∀ y ∈ x ∀ z ∈ x y + G z ∈ x$
18 1 15 oppgbas $⊢ Base G = Base O$
19 1 16 oppgid $⊢ 0 G = 0 O$
20 18 19 8 issubm $⊢ O ∈ Mnd → x ∈ SubMnd ⁡ O ↔ x ⊆ Base G ∧ 0 G ∈ x ∧ ∀ z ∈ x ∀ y ∈ x z + O y ∈ x$
21 4 20 sylbi $⊢ G ∈ Mnd → x ∈ SubMnd ⁡ O ↔ x ⊆ Base G ∧ 0 G ∈ x ∧ ∀ z ∈ x ∀ y ∈ x z + O y ∈ x$
22 14 17 21 3bitr4d $⊢ G ∈ Mnd → x ∈ SubMnd ⁡ G ↔ x ∈ SubMnd ⁡ O$
23 2 5 22 pm5.21nii $⊢ x ∈ SubMnd ⁡ G ↔ x ∈ SubMnd ⁡ O$
24 23 eqriv $⊢ SubMnd ⁡ G = SubMnd ⁡ O$