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	syl5req	⊢ ( 𝐼 ∈ 𝑉 → { ⟨ 𝐼 , 𝐼 ⟩ } = ( 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 ↾ { 𝐼 } ) )