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

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 ↾ { 𝐼 } ) )