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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
	odid.3	⊢ · = ( .g ‘ 𝐺 )
	odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	odid	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		odcl.1	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		odcl.2	⊢ 𝑂 = ( od ‘ 𝐺 )
3		odid.3	⊢ · = ( .g ‘ 𝐺 )
4		odid.4	⊢ 0 = ( 0g ‘ 𝐺 )
5		oveq1	⊢ ( ( 𝑂 ‘ 𝐴 ) = 0 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = ( 0 · 𝐴 ) )
6	1 4 3	mulg0	⊢ ( 𝐴 ∈ 𝑋 → ( 0 · 𝐴 ) = 0 )
7	5 6	sylan9eqr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) = 0 ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
8	7	adantrr	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( ( 𝑂 ‘ 𝐴 ) = 0 ∧ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = ∅ ) ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
9		oveq1	⊢ ( 𝑦 = ( 𝑂 ‘ 𝐴 ) → ( 𝑦 · 𝐴 ) = ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) )
10	9	eqeq1d	⊢ ( 𝑦 = ( 𝑂 ‘ 𝐴 ) → ( ( 𝑦 · 𝐴 ) = 0 ↔ ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) )
11	10	elrab	⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ↔ ( ( 𝑂 ‘ 𝐴 ) ∈ ℕ ∧ ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 ) )
12	11	simprbi	⊢ ( ( 𝑂 ‘ 𝐴 ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
13	12	adantl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ ( 𝑂 ‘ 𝐴 ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )
14		eqid	⊢ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 }
15	1 3 4 2 14	odlem1	⊢ ( 𝐴 ∈ 𝑋 → ( ( ( 𝑂 ‘ 𝐴 ) = 0 ∧ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } = ∅ ) ∨ ( 𝑂 ‘ 𝐴 ) ∈ { 𝑦 ∈ ℕ ∣ ( 𝑦 · 𝐴 ) = 0 } ) )
16	8 13 15	mpjaodan	⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = 0 )