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