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

Metamath Proof Explorer

Theorem odval2

Description: A non-conditional definition of the group order. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
odid.3 ⊢ · = ( .g ‘ 𝐺 )
odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion odval2 ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 odcl.1 ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odcl.2 ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odid.3 ⊢ · = ( .g ‘ 𝐺 )
4 odid.4 ⊢ 0 = ( 0g ‘ 𝐺 )
5 1 2 odcl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
6 5 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
7 1 2 3 4 odeq ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 = ( 𝑂 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )
8 7 3expa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ ℕ0 ) → ( 𝑥 = ( 𝑂 ‘ 𝐴 ) ↔ ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )
9 8 bicomd ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ ℕ0 ) → ( ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ↔ 𝑥 = ( 𝑂 ‘ 𝐴 ) ) )
10 6 9 riota5 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( ℩ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) = ( 𝑂 ‘ 𝐴 ) )
11 10 eqcomd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑂 ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℕ0 ∀ 𝑦 ∈ ℕ0 ( 𝑥 ∥ 𝑦 ↔ ( 𝑦 · 𝐴 ) = 0 ) ) )