Metamath Proof Explorer


Theorem grp1inv

Description: The inverse function of the trivial group. (Contributed by FL, 21-Jun-2010) (Revised by AV, 26-Aug-2021)

Ref Expression
Hypothesis grp1.m M = Base ndx I + ndx I I I
Assertion grp1inv I V inv g M = I I

Proof

Step Hyp Ref Expression
1 grp1.m M = Base ndx I + ndx I I I
2 1 grp1 I V M Grp
3 snex I V
4 1 grpbase I V I = Base M
5 3 4 ax-mp I = Base M
6 eqid inv g M = inv g M
7 5 6 grpinvf M Grp inv g M : I I
8 2 7 syl I V inv g M : I I
9 fsng I V I V inv g M : I I inv g M = I I
10 9 anidms I V inv g M : I I inv g M = I I
11 simpr I V inv g M = I I inv g M = I I
12 restidsing I I = I × I
13 xpsng I V I V I × I = I I
14 13 anidms I V I × I = I I
15 12 14 eqtr2id I V I I = I I
16 15 adantr I V inv g M = I I I I = I I
17 11 16 eqtrd I V inv g M = I I inv g M = I I
18 17 ex I V inv g M = I I inv g M = I I
19 10 18 sylbid I V inv g M : I I inv g M = I I
20 8 19 mpd I V inv g M = I I