# Metamath Proof Explorer

## Theorem cyggexb

Description: A finite abelian group is cyclic iff the exponent equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygctb.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
cyggex.o ${⊢}{E}=\mathrm{gEx}\left({G}\right)$
Assertion cyggexb ${⊢}\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\to \left({G}\in \mathrm{CycGrp}↔{E}=\left|{B}\right|\right)$

### Proof

Step Hyp Ref Expression
1 cygctb.1 ${⊢}{B}={\mathrm{Base}}_{{G}}$
2 cyggex.o ${⊢}{E}=\mathrm{gEx}\left({G}\right)$
3 1 2 cyggex ${⊢}\left({G}\in \mathrm{CycGrp}\wedge {B}\in \mathrm{Fin}\right)\to {E}=\left|{B}\right|$
4 3 expcom ${⊢}{B}\in \mathrm{Fin}\to \left({G}\in \mathrm{CycGrp}\to {E}=\left|{B}\right|\right)$
5 4 adantl ${⊢}\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\to \left({G}\in \mathrm{CycGrp}\to {E}=\left|{B}\right|\right)$
6 simpll ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to {G}\in \mathrm{Abel}$
7 ablgrp ${⊢}{G}\in \mathrm{Abel}\to {G}\in \mathrm{Grp}$
8 7 ad2antrr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to {G}\in \mathrm{Grp}$
9 simplr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to {B}\in \mathrm{Fin}$
10 1 2 gexcl2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {B}\in \mathrm{Fin}\right)\to {E}\in ℕ$
11 8 9 10 syl2anc ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to {E}\in ℕ$
12 eqid ${⊢}\mathrm{od}\left({G}\right)=\mathrm{od}\left({G}\right)$
13 1 2 12 gexex ${⊢}\left({G}\in \mathrm{Abel}\wedge {E}\in ℕ\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)={E}$
14 6 11 13 syl2anc ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to \exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)={E}$
15 simplr ${⊢}\left(\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\wedge {x}\in {B}\right)\to {E}=\left|{B}\right|$
16 15 eqeq2d ${⊢}\left(\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\wedge {x}\in {B}\right)\to \left(\mathrm{od}\left({G}\right)\left({x}\right)={E}↔\mathrm{od}\left({G}\right)\left({x}\right)=\left|{B}\right|\right)$
17 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
18 eqid ${⊢}\left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}=\left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}$
19 1 17 18 12 cyggenod ${⊢}\left({G}\in \mathrm{Grp}\wedge {B}\in \mathrm{Fin}\right)\to \left({x}\in \left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}↔\left({x}\in {B}\wedge \mathrm{od}\left({G}\right)\left({x}\right)=\left|{B}\right|\right)\right)$
20 8 9 19 syl2anc ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to \left({x}\in \left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}↔\left({x}\in {B}\wedge \mathrm{od}\left({G}\right)\left({x}\right)=\left|{B}\right|\right)\right)$
21 ne0i ${⊢}{x}\in \left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}\to \left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}\ne \varnothing$
22 1 17 18 iscyg2 ${⊢}{G}\in \mathrm{CycGrp}↔\left({G}\in \mathrm{Grp}\wedge \left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}\ne \varnothing \right)$
23 22 baib ${⊢}{G}\in \mathrm{Grp}\to \left({G}\in \mathrm{CycGrp}↔\left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}\ne \varnothing \right)$
24 8 23 syl ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to \left({G}\in \mathrm{CycGrp}↔\left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}\ne \varnothing \right)$
25 21 24 syl5ibr ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to \left({x}\in \left\{{y}\in {B}|\mathrm{ran}\left({n}\in ℤ⟼{n}{\cdot }_{{G}}{y}\right)={B}\right\}\to {G}\in \mathrm{CycGrp}\right)$
26 20 25 sylbird ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to \left(\left({x}\in {B}\wedge \mathrm{od}\left({G}\right)\left({x}\right)=\left|{B}\right|\right)\to {G}\in \mathrm{CycGrp}\right)$
27 26 expdimp ${⊢}\left(\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\wedge {x}\in {B}\right)\to \left(\mathrm{od}\left({G}\right)\left({x}\right)=\left|{B}\right|\to {G}\in \mathrm{CycGrp}\right)$
28 16 27 sylbid ${⊢}\left(\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\wedge {x}\in {B}\right)\to \left(\mathrm{od}\left({G}\right)\left({x}\right)={E}\to {G}\in \mathrm{CycGrp}\right)$
29 28 rexlimdva ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}\mathrm{od}\left({G}\right)\left({x}\right)={E}\to {G}\in \mathrm{CycGrp}\right)$
30 14 29 mpd ${⊢}\left(\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\wedge {E}=\left|{B}\right|\right)\to {G}\in \mathrm{CycGrp}$
31 30 ex ${⊢}\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\to \left({E}=\left|{B}\right|\to {G}\in \mathrm{CycGrp}\right)$
32 5 31 impbid ${⊢}\left({G}\in \mathrm{Abel}\wedge {B}\in \mathrm{Fin}\right)\to \left({G}\in \mathrm{CycGrp}↔{E}=\left|{B}\right|\right)$