Theorem gexval

Description: Value of the exponent of a group. (Contributed by Mario Carneiro, 23-Apr-2016) (Revised by AV, 26-Sep-2020)

	Ref	Expression
Hypotheses	gexval.1	$$⊢X={\mathrm{Base}}_G$$
	gexval.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	gexval.3	$$⊢\underset{\dot{}}{0}=0_G$$
	gexval.4	$$⊢E=\mathrm{gEx}\left(G\right)$$
	gexval.i	$$⊢I=\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
Assertion	gexval	$$⊢G\in V\to E=if\left(I=\varnothing ,0,sup\left(I,ℝ,<\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		gexval.1	$$⊢X={\mathrm{Base}}_G$$
2		gexval.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		gexval.3	$$⊢\underset{\dot{}}{0}=0_G$$
4		gexval.4	$$⊢E=\mathrm{gEx}\left(G\right)$$
5		gexval.i	$$⊢I=\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
6		df-gex	$$⊢\mathrm{gEx}=\left(g\in \mathrm{V}⟼⦋\left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,sup\left(i,ℝ,<\right)\right)\right)$$
7		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
8	7	rabex	$$⊢\left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}\in \mathrm{V}$$
9	8	a1i	$$⊢\left(G\in V\wedge g=G\right)\to \left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}\in \mathrm{V}$$
10		simpr	$$⊢\left(G\in V\wedge g=G\right)\to g=G$$
11	10	fveq2d	$$⊢\left(G\in V\wedge g=G\right)\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
12	11 1	syl6eqr	$$⊢\left(G\in V\wedge g=G\right)\to {\mathrm{Base}}_g=X$$
13	10	fveq2d	$$⊢\left(G\in V\wedge g=G\right)\to {\cdot }_g={\cdot }_G$$
14	13 2	syl6eqr	$$⊢\left(G\in V\wedge g=G\right)\to {\cdot }_g=\underset{\dot{}}{·}$$
15	14	oveqd	$$⊢\left(G\in V\wedge g=G\right)\to y{\cdot }_{g}x=y\underset{\dot{}}{·}x$$
16	10	fveq2d	$$⊢\left(G\in V\wedge g=G\right)\to 0_g=0_G$$
17	16 3	syl6eqr	$$⊢\left(G\in V\wedge g=G\right)\to 0_g=\underset{\dot{}}{0}$$
18	15 17	eqeq12d	$$⊢\left(G\in V\wedge g=G\right)\to \left(y{\cdot }_{g}x=0_g\leftrightarrow y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
19	12 18	raleqbidv	$$⊢\left(G\in V\wedge g=G\right)\to \left(\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\leftrightarrow \forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
20	19	rabbidv	$$⊢\left(G\in V\wedge g=G\right)\to \left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}=\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
21	20 5	syl6eqr	$$⊢\left(G\in V\wedge g=G\right)\to \left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}=I$$
22	21	eqeq2d	$$⊢\left(G\in V\wedge g=G\right)\to \left(i=\left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}\leftrightarrow i=I\right)$$
23	22	biimpa	$$⊢\left(\left(G\in V\wedge g=G\right)\wedge i=\left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}\right)\to i=I$$
24	23	eqeq1d	$$⊢\left(\left(G\in V\wedge g=G\right)\wedge i=\left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}\right)\to \left(i=\varnothing \leftrightarrow I=\varnothing \right)$$
25	23	infeq1d	$$⊢\left(\left(G\in V\wedge g=G\right)\wedge i=\left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}\right)\to sup\left(i,ℝ,<\right)=sup\left(I,ℝ,<\right)$$
26	24 25	ifbieq2d	$$⊢\left(\left(G\in V\wedge g=G\right)\wedge i=\left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}\right)\to if\left(i=\varnothing ,0,sup\left(i,ℝ,<\right)\right)=if\left(I=\varnothing ,0,sup\left(I,ℝ,<\right)\right)$$
27	9 26	csbied	$$⊢\left(G\in V\wedge g=G\right)\to ⦋\left\{y\in \mathbb{N}|\forall x\in {\mathrm{Base}}_{g}y{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,sup\left(i,ℝ,<\right)\right)=if\left(I=\varnothing ,0,sup\left(I,ℝ,<\right)\right)$$
28		elex	$$⊢G\in V\to G\in \mathrm{V}$$
29		c0ex	$$⊢0\in \mathrm{V}$$
30		ltso	$$⊢<\mathrm{Or}ℝ$$
31	30	infex	$$⊢sup\left(I,ℝ,<\right)\in \mathrm{V}$$
32	29 31	ifex	$$⊢if\left(I=\varnothing ,0,sup\left(I,ℝ,<\right)\right)\in \mathrm{V}$$
33	32	a1i	$$⊢G\in V\to if\left(I=\varnothing ,0,sup\left(I,ℝ,<\right)\right)\in \mathrm{V}$$
34	6 27 28 33	fvmptd2	$$⊢G\in V\to \mathrm{gEx}\left(G\right)=if\left(I=\varnothing ,0,sup\left(I,ℝ,<\right)\right)$$
35	4 34	syl5eq	$$⊢G\in V\to E=if\left(I=\varnothing ,0,sup\left(I,ℝ,<\right)\right)$$