Theorem gexlem1

Description: The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 23-Apr-2016) (Proof shortened 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	gexlem1	$$⊢G\in V\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\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	1 2 3 4 5	gexval	$$⊢G\in V\to E=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)$$
7		eqeq2	$$⊢0=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\to \left(E=0\leftrightarrow E=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\right)$$
8	7	imbi1d	$$⊢0=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\to \left(\left(E=0\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)\right)\leftrightarrow \left(E=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)\right)\right)$$
9		eqeq2	$$⊢inf\left(I,ℝ,<\right)=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\to \left(E=inf\left(I,ℝ,<\right)\leftrightarrow E=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\right)$$
10	9	imbi1d	$$⊢inf\left(I,ℝ,<\right)=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\to \left(\left(E=inf\left(I,ℝ,<\right)\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)\right)\leftrightarrow \left(E=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)\right)\right)$$
11		orc	$$⊢\left(E=0\wedge I=\varnothing \right)\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)$$
12	11	expcom	$$⊢I=\varnothing \to \left(E=0\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)\right)$$
13	12	adantl	$$⊢\left(G\in V\wedge I=\varnothing \right)\to \left(E=0\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)\right)$$
14		ssrab2	$$⊢\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\subseteq \mathbb{N}$$
15		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
16	15	eqcomi	$$⊢{\mathbb{Z}}_{\ge 1}=\mathbb{N}$$
17	14 5 16	3sstr4i	$$⊢I\subseteq {\mathbb{Z}}_{\ge 1}$$
18		neqne	$$⊢\neg I=\varnothing \to I\ne \varnothing$$
19	18	adantl	$$⊢\left(G\in V\wedge \neg I=\varnothing \right)\to I\ne \varnothing$$
20		infssuzcl	$$⊢\left(I\subseteq {\mathbb{Z}}_{\ge 1}\wedge I\ne \varnothing \right)\to inf\left(I,ℝ,<\right)\in I$$
21	17 19 20	sylancr	$$⊢\left(G\in V\wedge \neg I=\varnothing \right)\to inf\left(I,ℝ,<\right)\in I$$
22		eleq1a	$$⊢inf\left(I,ℝ,<\right)\in I\to \left(E=inf\left(I,ℝ,<\right)\to E\in I\right)$$
23	21 22	syl	$$⊢\left(G\in V\wedge \neg I=\varnothing \right)\to \left(E=inf\left(I,ℝ,<\right)\to E\in I\right)$$
24		olc	$$⊢E\in I\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)$$
25	23 24	syl6	$$⊢\left(G\in V\wedge \neg I=\varnothing \right)\to \left(E=inf\left(I,ℝ,<\right)\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)\right)$$
26	8 10 13 25	ifbothda	$$⊢G\in V\to \left(E=if\left(I=\varnothing ,0,inf\left(I,ℝ,<\right)\right)\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)\right)$$
27	6 26	mpd	$$⊢G\in V\to \left(\left(E=0\wedge I=\varnothing \right)\vee E\in I\right)$$