Theorem rlmvneg

Description: Vector negation in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014) (Revised by Mario Carneiro, 5-Jun-2015)

	Ref	Expression
Assertion	rlmvneg	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ ( ringLMod ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
2		rlmbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) )
3	2	a1i	⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ ( ringLMod ‘ 𝑅 ) ) )
4		rlmplusg	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) )
5	4	a1i	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( ringLMod ‘ 𝑅 ) ) )
6	5	oveqd	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( ringLMod ‘ 𝑅 ) ) 𝑦 ) )
7	1 3 6	grpinvpropd	⊢ ( ⊤ → ( invg ‘ 𝑅 ) = ( invg ‘ ( ringLMod ‘ 𝑅 ) ) )
8	7	mptru	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ ( ringLMod ‘ 𝑅 ) )