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 \in V \to {inv}_{g} (M) = {I ↾}_{\{I\}}$

Step	Hyp	Ref	Expression
1		grp1.m	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}$
2	1	grp1	$⊢ I \in V \to M \in Grp$
3		snex	$⊢ \{I\} \in V$
4	1	grpbase	$⊢ \{I\} \in V \to \{I\} = {Base}_{M}$
5	3 4	ax-mp	$⊢ \{I\} = {Base}_{M}$
6		eqid	$⊢ {inv}_{g} (M) = {inv}_{g} (M)$
7	5 6	grpinvf	$⊢ M \in Grp \to {inv}_{g} (M) : \{I\} ⟶ \{I\}$
8	2 7	syl	$⊢ I \in V \to {inv}_{g} (M) : \{I\} ⟶ \{I\}$
9		fsng	$⊢ (I \in V \land I \in V) \to ({inv}_{g} (M) : \{I\} ⟶ \{I\} \leftrightarrow {inv}_{g} (M) = \{⟨I, I⟩\})$
10	9	anidms	$⊢ I \in V \to ({inv}_{g} (M) : \{I\} ⟶ \{I\} \leftrightarrow {inv}_{g} (M) = \{⟨I, I⟩\})$
11		simpr	$⊢ (I \in V \land {inv}_{g} (M) = \{⟨I, I⟩\}) \to {inv}_{g} (M) = \{⟨I, I⟩\}$
12		restidsing	$⊢ {I ↾}_{\{I\}} = \{I\} \times \{I\}$
13		xpsng	$⊢ (I \in V \land I \in V) \to \{I\} \times \{I\} = \{⟨I, I⟩\}$
14	13	anidms	$⊢ I \in V \to \{I\} \times \{I\} = \{⟨I, I⟩\}$
15	12 14	syl5req	$⊢ I \in V \to \{⟨I, I⟩\} = {I ↾}_{\{I\}}$
16	15	adantr	$⊢ (I \in V \land {inv}_{g} (M) = \{⟨I, I⟩\}) \to \{⟨I, I⟩\} = {I ↾}_{\{I\}}$
17	11 16	eqtrd	$⊢ (I \in V \land {inv}_{g} (M) = \{⟨I, I⟩\}) \to {inv}_{g} (M) = {I ↾}_{\{I\}}$
18	17	ex	$⊢ I \in V \to ({inv}_{g} (M) = \{⟨I, I⟩\} \to {inv}_{g} (M) = {I ↾}_{\{I\}})$
19	10 18	sylbid	$⊢ I \in V \to ({inv}_{g} (M) : \{I\} ⟶ \{I\} \to {inv}_{g} (M) = {I ↾}_{\{I\}})$
20	8 19	mpd	$⊢ I \in V \to {inv}_{g} (M) = {I ↾}_{\{I\}}$

Metamath Proof Explorer