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

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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringneglmul.t ⊢ · = ( .r ‘ 𝑅 )
ringneglmul.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
ringneglmul.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ringneglmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ringneglmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion ringm2neg ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑋 · 𝑌 ) )

Proof

Step Hyp Ref Expression
1 ringneglmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringneglmul.t ⊢ · = ( .r ‘ 𝑅 )
3 ringneglmul.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
4 ringneglmul.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 ringneglmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 ringneglmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 ringrng ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
8 4 7 syl ⊢ ( 𝜑 → 𝑅 ∈ Rng )
9 1 2 3 8 5 6 rngm2neg ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑋 · 𝑌 ) )