Definition df-od

Description: Define the order of an element in a group. (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by Stefan O'Rear, 4-Sep-2015) (Revised by AV, 5-Oct-2020)

	Ref	Expression
Assertion	df-od	$$⊢\mathrm{od}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼⦋\left\{n\in \mathbb{N}|n{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cod	$$class\mathrm{od}$$
1		vg	$$setvarg$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class{\mathrm{Base}}_g$$
7		vn	$$setvarn$$
8		cn	$$class\mathbb{N}$$
9	7	cv	$$setvarn$$
10		cmg	$$class{\mathrm{\cdot }}_{𝑔}$$
11	5 10	cfv	$$class{\cdot }_g$$
12	3	cv	$$setvarx$$
13	9 12 11	co	$$class\left(n{\cdot }_{g}x\right)$$
14		c0g	$$class{0}_{𝑔}$$
15	5 14	cfv	$$class{0}_g$$
16	13 15	wceq	$$wffn{\cdot }_{g}x=0_g$$
17	16 7 8	crab	$$class\left\{n\in \mathbb{N}|n{\cdot }_{g}x=0_g\right\}$$
18		vi	$$setvari$$
19	18	cv	$$setvari$$
20		c0	$$class\varnothing$$
21	19 20	wceq	$$wffi=\varnothing$$
22		cc0	$$class0$$
23		cr	$$classℝ$$
24		clt	$$class<$$
25	19 23 24	cinf	$$classinf\left(i,ℝ,<\right)$$
26	21 22 25	cif	$$classif\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)$$
27	18 17 26	csb	$$class⦋\left\{n\in \mathbb{N}|n{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)$$
28	3 6 27	cmpt	$$class\left(x\in {\mathrm{Base}}_g⟼⦋\left\{n\in \mathbb{N}|n{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)$$
29	1 2 28	cmpt	$$class\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼⦋\left\{n\in \mathbb{N}|n{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)\right)$$
30	0 29	wceq	$$wff\mathrm{od}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼⦋\left\{n\in \mathbb{N}|n{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)\right)$$