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