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 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
Assertion grp1inv ( 𝐼𝑉 → ( invg𝑀 ) = ( I ↾ { 𝐼 } ) )

Proof

Step Hyp Ref Expression
1 grp1.m 𝑀 = { ⟨ ( Base ‘ ndx ) , { 𝐼 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝐼 , 𝐼 ⟩ , 𝐼 ⟩ } ⟩ }
2 1 grp1 ( 𝐼𝑉𝑀 ∈ Grp )
3 snex { 𝐼 } ∈ V
4 1 grpbase ( { 𝐼 } ∈ V → { 𝐼 } = ( Base ‘ 𝑀 ) )
5 3 4 ax-mp { 𝐼 } = ( Base ‘ 𝑀 )
6 eqid ( invg𝑀 ) = ( invg𝑀 )
7 5 6 grpinvf ( 𝑀 ∈ Grp → ( invg𝑀 ) : { 𝐼 } ⟶ { 𝐼 } )
8 2 7 syl ( 𝐼𝑉 → ( invg𝑀 ) : { 𝐼 } ⟶ { 𝐼 } )
9 fsng ( ( 𝐼𝑉𝐼𝑉 ) → ( ( invg𝑀 ) : { 𝐼 } ⟶ { 𝐼 } ↔ ( invg𝑀 ) = { ⟨ 𝐼 , 𝐼 ⟩ } ) )
10 9 anidms ( 𝐼𝑉 → ( ( invg𝑀 ) : { 𝐼 } ⟶ { 𝐼 } ↔ ( invg𝑀 ) = { ⟨ 𝐼 , 𝐼 ⟩ } ) )
11 simpr ( ( 𝐼𝑉 ∧ ( invg𝑀 ) = { ⟨ 𝐼 , 𝐼 ⟩ } ) → ( invg𝑀 ) = { ⟨ 𝐼 , 𝐼 ⟩ } )
12 restidsing ( I ↾ { 𝐼 } ) = ( { 𝐼 } × { 𝐼 } )
13 xpsng ( ( 𝐼𝑉𝐼𝑉 ) → ( { 𝐼 } × { 𝐼 } ) = { ⟨ 𝐼 , 𝐼 ⟩ } )
14 13 anidms ( 𝐼𝑉 → ( { 𝐼 } × { 𝐼 } ) = { ⟨ 𝐼 , 𝐼 ⟩ } )
15 12 14 eqtr2id ( 𝐼𝑉 → { ⟨ 𝐼 , 𝐼 ⟩ } = ( I ↾ { 𝐼 } ) )
16 15 adantr ( ( 𝐼𝑉 ∧ ( invg𝑀 ) = { ⟨ 𝐼 , 𝐼 ⟩ } ) → { ⟨ 𝐼 , 𝐼 ⟩ } = ( I ↾ { 𝐼 } ) )
17 11 16 eqtrd ( ( 𝐼𝑉 ∧ ( invg𝑀 ) = { ⟨ 𝐼 , 𝐼 ⟩ } ) → ( invg𝑀 ) = ( I ↾ { 𝐼 } ) )
18 17 ex ( 𝐼𝑉 → ( ( invg𝑀 ) = { ⟨ 𝐼 , 𝐼 ⟩ } → ( invg𝑀 ) = ( I ↾ { 𝐼 } ) ) )
19 10 18 sylbid ( 𝐼𝑉 → ( ( invg𝑀 ) : { 𝐼 } ⟶ { 𝐼 } → ( invg𝑀 ) = ( I ↾ { 𝐼 } ) ) )
20 8 19 mpd ( 𝐼𝑉 → ( invg𝑀 ) = ( I ↾ { 𝐼 } ) )