Metamath Proof Explorer

Theorem linvh

Description: If an element has a unique left inverse, then the value satisfies the left inverse value equation. (Contributed by metakunt, 25-Apr-2025)

		Ref	Expression
	Hypotheses	linvh.1	$⊢ φ \to X \in {Base}_{R}$
		linvh.2	$⊢ φ \to \exists! i \in {Base}_{R} i +_{R} X = 0_{R}$
	Assertion	linvh	$⊢ φ \to {inv}_{g} (R) (X) +_{R} X = 0_{R}$

Proof

Step	Hyp	Ref	Expression
1		linvh.1	$⊢ φ \to X \in {Base}_{R}$
2		linvh.2	$⊢ φ \to \exists! i \in {Base}_{R} i +_{R} X = 0_{R}$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4		eqid	$⊢ +_{R} = +_{R}$
5		eqid	$⊢ 0_{R} = 0_{R}$
6		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
7	3 4 5 6	grpinvval	$⊢ X \in {Base}_{R} \to {inv}_{g} (R) (X) = (ι i \in {Base}_{R} \| i +_{R} X = 0_{R})$
8	1 7	syl	$⊢ φ \to {inv}_{g} (R) (X) = (ι i \in {Base}_{R} \| i +_{R} X = 0_{R})$
9		riotacl2	$⊢ \exists! i \in {Base}_{R} i +_{R} X = 0_{R} \to (ι i \in {Base}_{R} \| i +_{R} X = 0_{R}) \in \{i \in {Base}_{R} \| i +_{R} X = 0_{R}\}$
10	2 9	syl	$⊢ φ \to (ι i \in {Base}_{R} \| i +_{R} X = 0_{R}) \in \{i \in {Base}_{R} \| i +_{R} X = 0_{R}\}$
11	8 10	eqeltrd	$⊢ φ \to {inv}_{g} (R) (X) \in \{i \in {Base}_{R} \| i +_{R} X = 0_{R}\}$
12		oveq1	$⊢ i = {inv}_{g} (R) (X) \to i +_{R} X = {inv}_{g} (R) (X) +_{R} X$
13	12	eqeq1d	$⊢ i = {inv}_{g} (R) (X) \to (i +_{R} X = 0_{R} \leftrightarrow {inv}_{g} (R) (X) +_{R} X = 0_{R})$
14	13	elrab	$⊢ {inv}_{g} (R) (X) \in \{i \in {Base}_{R} \| i +_{R} X = 0_{R}\} \leftrightarrow ({inv}_{g} (R) (X) \in {Base}_{R} \land {inv}_{g} (R) (X) +_{R} X = 0_{R})$
15	14	simprbi	$⊢ {inv}_{g} (R) (X) \in \{i \in {Base}_{R} \| i +_{R} X = 0_{R}\} \to {inv}_{g} (R) (X) +_{R} X = 0_{R}$
16	11 15	syl	$⊢ φ \to {inv}_{g} (R) (X) +_{R} X = 0_{R}$