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

Metamath Proof Explorer

Theorem rngm2neg

Description: Double negation of a product in a non-unital ring ( mul2neg analog). (Contributed by Mario Carneiro, 4-Dec-2014) Generalization of ringm2neg . (Revised by AV, 17-Feb-2025)

Ref Expression
Hypotheses rngneglmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rngneglmul.t ⊢ · = ( .r ‘ 𝑅 )
rngneglmul.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
rngneglmul.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
rngneglmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
rngneglmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion rngm2neg ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑋 · 𝑌 ) )

Proof

Step Hyp Ref Expression
1 rngneglmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rngneglmul.t ⊢ · = ( .r ‘ 𝑅 )
3 rngneglmul.n ⊢ 𝑁 = ( invg ‘ 𝑅 )
4 rngneglmul.r ⊢ ( 𝜑 → 𝑅 ∈ Rng )
5 rngneglmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 rngneglmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
8 4 7 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
9 1 3 8 6 grpinvcld ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
10 1 2 3 4 5 9 rngmneg1 ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑁 ‘ ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ) )
11 1 2 3 4 5 6 rngmneg2 ⊢ ( 𝜑 → ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )
12 11 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ) = ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) ) )
13 1 2 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
14 4 5 6 13 syl3anc ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
15 1 3 grpinvinv ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) ) = ( 𝑋 · 𝑌 ) )
16 8 14 15 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) ) = ( 𝑋 · 𝑌 ) )
17 10 12 16 3eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑋 ) · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑋 · 𝑌 ) )