Theorem gexid

Description: Any element to the power of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016)

	Ref	Expression
Hypotheses	gexcl.1	$$⊢X={\mathrm{Base}}_G$$
	gexcl.2	$$⊢E=\mathrm{gEx}\left(G\right)$$
	gexid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	gexid.4	$$⊢\underset{\dot{}}{0}=0_G$$
Assertion	gexid	$$⊢A\in X\to E\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		gexcl.1	$$⊢X={\mathrm{Base}}_G$$
2		gexcl.2	$$⊢E=\mathrm{gEx}\left(G\right)$$
3		gexid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		gexid.4	$$⊢\underset{\dot{}}{0}=0_G$$
5		oveq1	$$⊢E=0\to E\underset{\dot{}}{·}A=0\underset{\dot{}}{·}A$$
6	1 4 3	mulg0	$$⊢A\in X\to 0\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
7	5 6	sylan9eqr	$$⊢\left(A\in X\wedge E=0\right)\to E\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
8	7	adantrr	$$⊢\left(A\in X\wedge \left(E=0\wedge \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing \right)\right)\to E\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
9		oveq1	$$⊢y=E\to y\underset{\dot{}}{·}x=E\underset{\dot{}}{·}x$$
10	9	eqeq1d	$$⊢y=E\to \left(y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\leftrightarrow E\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
11	10	ralbidv	$$⊢y=E\to \left(\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\leftrightarrow \forall x\in XE\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
12	11	elrab	$$⊢E\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\leftrightarrow \left(E\in \mathbb{N}\wedge \forall x\in XE\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
13	12	simprbi	$$⊢E\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to \forall x\in XE\underset{\dot{}}{·}x=\underset{\dot{}}{0}$$
14		oveq2	$$⊢x=A\to E\underset{\dot{}}{·}x=E\underset{\dot{}}{·}A$$
15	14	eqeq1d	$$⊢x=A\to \left(E\underset{\dot{}}{·}x=\underset{\dot{}}{0}\leftrightarrow E\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
16	15	rspcva	$$⊢\left(A\in X\wedge \forall x\in XE\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)\to E\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
17	13 16	sylan2	$$⊢\left(A\in X\wedge E\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)\to E\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
18		elfvex	$$⊢A\in {\mathrm{Base}}_G\to G\in \mathrm{V}$$
19	18 1	eleq2s	$$⊢A\in X\to G\in \mathrm{V}$$
20		eqid	$$⊢\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
21	1 3 4 2 20	gexlem1	$$⊢G\in \mathrm{V}\to \left(\left(E=0\wedge \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing \right)\vee E\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)$$
22	19 21	syl	$$⊢A\in X\to \left(\left(E=0\wedge \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing \right)\vee E\in \left\{y\in \mathbb{N}|\forall x\in Xy\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\right)$$
23	8 17 22	mpjaodan	$$⊢A\in X\to E\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$