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

Metamath Proof Explorer

Theorem odm1inv

Description: The (order-1)th multiple of an element is its inverse. (Contributed by SN, 31-Jan-2025)

Ref Expression
Hypotheses odm1inv.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
odm1inv.o ⊢ 𝑂 = ( od ‘ 𝐺 )
odm1inv.t ⊢ · = ( .g ‘ 𝐺 )
odm1inv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
odm1inv.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
odm1inv.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
Assertion odm1inv ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) − 1 ) · 𝐴 ) = ( 𝐼 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 odm1inv.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 odm1inv.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 odm1inv.t ⊢ · = ( .g ‘ 𝐺 )
4 odm1inv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
5 odm1inv.g ⊢ ( 𝜑 → 𝐺 ∈ Grp )
6 odm1inv.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
7 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
8 1 2 3 7 odid ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) )
9 6 8 syl ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) = ( 0g ‘ 𝐺 ) )
10 1 3 mulg1 ⊢ ( 𝐴 ∈ 𝑋 → ( 1 · 𝐴 ) = 𝐴 )
11 6 10 syl ⊢ ( 𝜑 → ( 1 · 𝐴 ) = 𝐴 )
12 9 11 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ( -g ‘ 𝐺 ) ( 1 · 𝐴 ) ) = ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) )
13 1 2 6 odcld ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℕ0 )
14 13 nn0zd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) ∈ ℤ )
15 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
16 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
17 1 3 16 mulgsubdir ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑂 ‘ 𝐴 ) ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( 𝑂 ‘ 𝐴 ) − 1 ) · 𝐴 ) = ( ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ( -g ‘ 𝐺 ) ( 1 · 𝐴 ) ) )
18 5 14 15 6 17 syl13anc ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) − 1 ) · 𝐴 ) = ( ( ( 𝑂 ‘ 𝐴 ) · 𝐴 ) ( -g ‘ 𝐺 ) ( 1 · 𝐴 ) ) )
19 1 16 4 7 grpinvval2 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐼 ‘ 𝐴 ) = ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) )
20 5 6 19 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝐴 ) = ( ( 0g ‘ 𝐺 ) ( -g ‘ 𝐺 ) 𝐴 ) )
21 12 18 20 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑂 ‘ 𝐴 ) − 1 ) · 𝐴 ) = ( 𝐼 ‘ 𝐴 ) )