# Metamath Proof Explorer

## Theorem odhash3

Description: An element which generates a finite subgroup has order the size of that subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses odhash.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
odhash.o ${⊢}{O}=\mathrm{od}\left({G}\right)$
odhash.k ${⊢}{K}=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)$
Assertion odhash3 ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {K}\left(\left\{{A}\right\}\right)\in \mathrm{Fin}\right)\to {O}\left({A}\right)=\left|{K}\left(\left\{{A}\right\}\right)\right|$

### Proof

Step Hyp Ref Expression
1 odhash.x ${⊢}{X}={\mathrm{Base}}_{{G}}$
2 odhash.o ${⊢}{O}=\mathrm{od}\left({G}\right)$
3 odhash.k ${⊢}{K}=\mathrm{mrCls}\left(\mathrm{SubGrp}\left({G}\right)\right)$
4 1 2 odcl ${⊢}{A}\in {X}\to {O}\left({A}\right)\in {ℕ}_{0}$
5 4 3ad2ant2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {K}\left(\left\{{A}\right\}\right)\in \mathrm{Fin}\right)\to {O}\left({A}\right)\in {ℕ}_{0}$
6 hashcl ${⊢}{K}\left(\left\{{A}\right\}\right)\in \mathrm{Fin}\to \left|{K}\left(\left\{{A}\right\}\right)\right|\in {ℕ}_{0}$
7 6 nn0red ${⊢}{K}\left(\left\{{A}\right\}\right)\in \mathrm{Fin}\to \left|{K}\left(\left\{{A}\right\}\right)\right|\in ℝ$
8 pnfnre ${⊢}\mathrm{+\infty }\notin ℝ$
9 8 neli ${⊢}¬\mathrm{+\infty }\in ℝ$
10 1 2 3 odhash ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to \left|{K}\left(\left\{{A}\right\}\right)\right|=\mathrm{+\infty }$
11 10 eleq1d ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to \left(\left|{K}\left(\left\{{A}\right\}\right)\right|\in ℝ↔\mathrm{+\infty }\in ℝ\right)$
12 9 11 mtbiri ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)=0\right)\to ¬\left|{K}\left(\left\{{A}\right\}\right)\right|\in ℝ$
13 12 3expia ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\right)\to \left({O}\left({A}\right)=0\to ¬\left|{K}\left(\left\{{A}\right\}\right)\right|\in ℝ\right)$
14 13 necon2ad ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\right)\to \left(\left|{K}\left(\left\{{A}\right\}\right)\right|\in ℝ\to {O}\left({A}\right)\ne 0\right)$
15 7 14 syl5 ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\right)\to \left({K}\left(\left\{{A}\right\}\right)\in \mathrm{Fin}\to {O}\left({A}\right)\ne 0\right)$
16 15 3impia ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {K}\left(\left\{{A}\right\}\right)\in \mathrm{Fin}\right)\to {O}\left({A}\right)\ne 0$
17 elnnne0 ${⊢}{O}\left({A}\right)\in ℕ↔\left({O}\left({A}\right)\in {ℕ}_{0}\wedge {O}\left({A}\right)\ne 0\right)$
18 5 16 17 sylanbrc ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {K}\left(\left\{{A}\right\}\right)\in \mathrm{Fin}\right)\to {O}\left({A}\right)\in ℕ$
19 1 2 3 odhash2 ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {O}\left({A}\right)\in ℕ\right)\to \left|{K}\left(\left\{{A}\right\}\right)\right|={O}\left({A}\right)$
20 18 19 syld3an3 ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {K}\left(\left\{{A}\right\}\right)\in \mathrm{Fin}\right)\to \left|{K}\left(\left\{{A}\right\}\right)\right|={O}\left({A}\right)$
21 20 eqcomd ${⊢}\left({G}\in \mathrm{Grp}\wedge {A}\in {X}\wedge {K}\left(\left\{{A}\right\}\right)\in \mathrm{Fin}\right)\to {O}\left({A}\right)=\left|{K}\left(\left\{{A}\right\}\right)\right|$