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	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
	linvh.2	⊢ ( 𝜑 → ∃! 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) )
Assertion	linvh	⊢ ( 𝜑 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		linvh.1	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
2		linvh.2	⊢ ( 𝜑 → ∃! 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
5		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6		eqid	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
7	3 4 5 6	grpinvval	⊢ ( 𝑋 ∈ ( Base ‘ 𝑅 ) → ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) = ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) ) )
8	1 7	syl	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) = ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) ) )
9		riotacl2	⊢ ( ∃! 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) → ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) ) ∈ { 𝑖 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) } )
10	2 9	syl	⊢ ( 𝜑 → ( ℩ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) ) ∈ { 𝑖 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) } )
11	8 10	eqeltrd	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ∈ { 𝑖 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) } )
12		oveq1	⊢ ( 𝑖 = ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) → ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) )
13	12	eqeq1d	⊢ ( 𝑖 = ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) ↔ ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) ) )
14	13	elrab	⊢ ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ∈ { 𝑖 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) } ↔ ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) ) )
15	14	simprbi	⊢ ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ∈ { 𝑖 ∈ ( Base ‘ 𝑅 ) ∣ ( 𝑖 ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) } → ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) )
16	11 15	syl	⊢ ( 𝜑 → ( ( ( invg ‘ 𝑅 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) 𝑋 ) = ( 0g ‘ 𝑅 ) )