Theorem odid

Description: Any element to the power of its order is the identity. (Contributed by Mario Carneiro, 14-Jan-2015) (Revised by Stefan O'Rear, 5-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		odcl.1	$$⊢X={\mathrm{Base}}_G$$
2		odcl.2	$$⊢O=\mathrm{od}\left(G\right)$$
3		odid.3	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
4		odid.4	$$⊢\underset{\dot{}}{0}=0_G$$
5		oveq1	$$⊢O\left(A\right)=0\to O\left(A\right)\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 O\left(A\right)=0\right)\to O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
8	7	adantrr	$$⊢\left(A\in X\wedge \left(O\left(A\right)=0\wedge \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}=\varnothing \right)\right)\to O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
9		oveq1	$$⊢y=O\left(A\right)\to y\underset{\dot{}}{·}A=O\left(A\right)\underset{\dot{}}{·}A$$
10	9	eqeq1d	$$⊢y=O\left(A\right)\to \left(y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\leftrightarrow O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
11	10	elrab	$$⊢O\left(A\right)\in \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}\leftrightarrow \left(O\left(A\right)\in \mathbb{N}\wedge O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right)$$
12	11	simprbi	$$⊢O\left(A\right)\in \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}\to O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
13	12	adantl	$$⊢\left(A\in X\wedge O\left(A\right)\in \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}\right)\to O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$
14		eqid	$$⊢\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}=\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}$$
15	1 3 4 2 14	odlem1	$$⊢A\in X\to \left(\left(O\left(A\right)=0\wedge \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}=\varnothing \right)\vee O\left(A\right)\in \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}A=\underset{\dot{}}{0}\right\}\right)$$
16	8 13 15	mpjaodan	$$⊢A\in X\to O\left(A\right)\underset{\dot{}}{·}A=\underset{\dot{}}{0}$$