Metamath Proof Explorer


Theorem finsubmsubg

Description: A submonoid of a finite group is a subgroup. This does not extend to infinite groups, as the submonoid NN0 of the group ( ZZ , + ) shows. Note also that the union of a submonoid and its inverses need not be a submonoid, as the submonoid ( NN0 \ { 1 } ) of the group ( ZZ , + ) shows: 3 is in that submonoid, -2 is the inverse of 2, but 1 is not in their union. Or simply, the subgroup generated by ( NN0 \ { 1 } ) is ZZ , not ( ZZ \ { 1 , -u 1 } ) . (Contributed by SN, 31-Jan-2025)

Ref Expression
Hypotheses finsubmsubg.b B = Base G
finsubmsubg.g φ G Grp
finsubmsubg.s φ S SubMnd G
finsubmsubg.1 φ B Fin
Assertion finsubmsubg φ S SubGrp G

Proof

Step Hyp Ref Expression
1 finsubmsubg.b B = Base G
2 finsubmsubg.g φ G Grp
3 finsubmsubg.s φ S SubMnd G
4 finsubmsubg.1 φ B Fin
5 eqid od G = od G
6 2 adantr φ a S G Grp
7 4 adantr φ a S B Fin
8 1 submss S SubMnd G S B
9 3 8 syl φ S B
10 9 sselda φ a S a B
11 1 5 odcl2 G Grp B Fin a B od G a
12 6 7 10 11 syl3anc φ a S od G a
13 12 ralrimiva φ a S od G a
14 5 2 3 13 finodsubmsubg φ S SubGrp G