Metamath Proof Explorer


Theorem issubg3

Description: A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis issubg3.i I = inv g G
Assertion issubg3 G Grp S SubGrp G S SubMnd G x S I x S

Proof

Step Hyp Ref Expression
1 issubg3.i I = inv g G
2 eqid 0 G = 0 G
3 2 subg0cl S SubGrp G 0 G S
4 3 a1i G Grp S SubGrp G 0 G S
5 2 subm0cl S SubMnd G 0 G S
6 5 adantr S SubMnd G x S I x S 0 G S
7 6 a1i G Grp S SubMnd G x S I x S 0 G S
8 ne0i 0 G S S
9 id 0 G S 0 G S
10 8 9 2thd 0 G S S 0 G S
11 10 adantl G Grp 0 G S S 0 G S
12 r19.26 x S y S x + G y S I x S x S y S x + G y S x S I x S
13 12 a1i G Grp 0 G S x S y S x + G y S I x S x S y S x + G y S x S I x S
14 11 13 3anbi23d G Grp 0 G S S Base G S x S y S x + G y S I x S S Base G 0 G S x S y S x + G y S x S I x S
15 anass S Base G 0 G S x S y S x + G y S x S I x S S Base G 0 G S x S y S x + G y S x S I x S
16 df-3an S Base G 0 G S x S y S x + G y S S Base G 0 G S x S y S x + G y S
17 16 anbi1i S Base G 0 G S x S y S x + G y S x S I x S S Base G 0 G S x S y S x + G y S x S I x S
18 df-3an S Base G 0 G S x S y S x + G y S x S I x S S Base G 0 G S x S y S x + G y S x S I x S
19 15 17 18 3bitr4ri S Base G 0 G S x S y S x + G y S x S I x S S Base G 0 G S x S y S x + G y S x S I x S
20 14 19 bitrdi G Grp 0 G S S Base G S x S y S x + G y S I x S S Base G 0 G S x S y S x + G y S x S I x S
21 eqid Base G = Base G
22 eqid + G = + G
23 21 22 1 issubg2 G Grp S SubGrp G S Base G S x S y S x + G y S I x S
24 23 adantr G Grp 0 G S S SubGrp G S Base G S x S y S x + G y S I x S
25 grpmnd G Grp G Mnd
26 21 2 22 issubm G Mnd S SubMnd G S Base G 0 G S x S y S x + G y S
27 25 26 syl G Grp S SubMnd G S Base G 0 G S x S y S x + G y S
28 27 anbi1d G Grp S SubMnd G x S I x S S Base G 0 G S x S y S x + G y S x S I x S
29 28 adantr G Grp 0 G S S SubMnd G x S I x S S Base G 0 G S x S y S x + G y S x S I x S
30 20 24 29 3bitr4d G Grp 0 G S S SubGrp G S SubMnd G x S I x S
31 30 ex G Grp 0 G S S SubGrp G S SubMnd G x S I x S
32 4 7 31 pm5.21ndd G Grp S SubGrp G S SubMnd G x S I x S