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 ⊢ X = Base G
odm1inv.o ⊢ O = od ⁡ G
odm1inv.t ⊢ · ˙ = ⋅ G
odm1inv.i ⊢ I = inv g ⁡ G
odm1inv.g ⊢ φ → G ∈ Grp
odm1inv.1 ⊢ φ → A ∈ X
Assertion odm1inv ⊢ φ → O ⁡ A − 1 · ˙ A = I ⁡ A

Proof

Step Hyp Ref Expression
1 odm1inv.x ⊢ X = Base G
2 odm1inv.o ⊢ O = od ⁡ G
3 odm1inv.t ⊢ · ˙ = ⋅ G
4 odm1inv.i ⊢ I = inv g ⁡ G
5 odm1inv.g ⊢ φ → G ∈ Grp
6 odm1inv.1 ⊢ φ → A ∈ X
7 eqid ⊢ 0 G = 0 G
8 1 2 3 7 odid ⊢ A ∈ X → O ⁡ A · ˙ A = 0 G
9 6 8 syl ⊢ φ → O ⁡ A · ˙ A = 0 G
10 1 3 mulg1 ⊢ A ∈ X → 1 · ˙ A = A
11 6 10 syl ⊢ φ → 1 · ˙ A = A
12 9 11 oveq12d ⊢ φ → O ⁡ A · ˙ A - G 1 · ˙ A = 0 G - G A
13 1 2 6 odcld ⊢ φ → O ⁡ A ∈ ℕ 0
14 13 nn0zd ⊢ φ → O ⁡ A ∈ ℤ
15 1zzd ⊢ φ → 1 ∈ ℤ
16 eqid ⊢ - G = - G
17 1 3 16 mulgsubdir ⊢ G ∈ Grp ∧ O ⁡ A ∈ ℤ ∧ 1 ∈ ℤ ∧ A ∈ X → O ⁡ A − 1 · ˙ A = O ⁡ A · ˙ A - G 1 · ˙ A
18 5 14 15 6 17 syl13anc ⊢ φ → O ⁡ A − 1 · ˙ A = O ⁡ A · ˙ A - G 1 · ˙ A
19 1 16 4 7 grpinvval2 ⊢ G ∈ Grp ∧ A ∈ X → I ⁡ A = 0 G - G A
20 5 6 19 syl2anc ⊢ φ → I ⁡ A = 0 G - G A
21 12 18 20 3eqtr4d ⊢ φ → O ⁡ A − 1 · ˙ A = I ⁡ A