Metamath Proof Explorer


Theorem ringm2neg

Description: Double negation of a product in a ring. ( mul2neg analog.) (Contributed by Mario Carneiro, 4-Dec-2014) (Proof shortened by AV, 30-Mar-2025)

Ref Expression
Hypotheses ringneglmul.b B = Base R
ringneglmul.t · ˙ = R
ringneglmul.n N = inv g R
ringneglmul.r φ R Ring
ringneglmul.x φ X B
ringneglmul.y φ Y B
Assertion ringm2neg φ N X · ˙ N Y = X · ˙ Y

Proof

Step Hyp Ref Expression
1 ringneglmul.b B = Base R
2 ringneglmul.t · ˙ = R
3 ringneglmul.n N = inv g R
4 ringneglmul.r φ R Ring
5 ringneglmul.x φ X B
6 ringneglmul.y φ Y B
7 ringrng R Ring R Rng
8 4 7 syl φ R Rng
9 1 2 3 8 5 6 rngm2neg φ N X · ˙ N Y = X · ˙ Y