This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑅 ) )