This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )