Database
BASIC ALGEBRAIC STRUCTURES
Rings
Unital rings
ringm2neg
Metamath Proof Explorer
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