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 SubMndG=SubMndO

Proof

Step Hyp Ref Expression
1 oppggic.o O=opp𝑔G
2 submrcl xSubMndGGMnd
3 submrcl xSubMndOOMnd
4 1 oppgmndb GMndOMnd
5 3 4 sylibr xSubMndOGMnd
6 ralcom yxzxy+Gzxzxyxy+Gzx
7 eqid +G=+G
8 eqid +O=+O
9 7 1 8 oppgplus z+Oy=y+Gz
10 9 eleq1i z+Oyxy+Gzx
11 10 2ralbii zxyxz+Oyxzxyxy+Gzx
12 6 11 bitr4i yxzxy+Gzxzxyxz+Oyx
13 12 3anbi3i xBaseG0Gxyxzxy+GzxxBaseG0Gxzxyxz+Oyx
14 13 a1i GMndxBaseG0Gxyxzxy+GzxxBaseG0Gxzxyxz+Oyx
15 eqid BaseG=BaseG
16 eqid 0G=0G
17 15 16 7 issubm GMndxSubMndGxBaseG0Gxyxzxy+Gzx
18 1 15 oppgbas BaseG=BaseO
19 1 16 oppgid 0G=0O
20 18 19 8 issubm OMndxSubMndOxBaseG0Gxzxyxz+Oyx
21 4 20 sylbi GMndxSubMndOxBaseG0Gxzxyxz+Oyx
22 14 17 21 3bitr4d GMndxSubMndGxSubMndO
23 2 5 22 pm5.21nii xSubMndGxSubMndO
24 23 eqriv SubMndG=SubMndO