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

Metamath Proof Explorer

Theorem rngmneg2

Description: Negation of a product in a non-unital ring ( mulneg2 analog). In contrast to ringmneg2 , the proof does not (and cannot) make use of the existence of a ring unity. (Contributed 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 rngmneg2 ( 𝜑 → ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )

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 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
8 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
10 4 9 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
11 1 7 8 3 10 6 grplinvd ⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝑌 ) ( +g ‘ 𝑅 ) 𝑌 ) = ( 0g ‘ 𝑅 ) )
12 11 oveq2d ⊢ ( 𝜑 → ( 𝑋 · ( ( 𝑁 ‘ 𝑌 ) ( +g ‘ 𝑅 ) 𝑌 ) ) = ( 𝑋 · ( 0g ‘ 𝑅 ) ) )
13 1 2 8 rngrz ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
14 4 5 13 syl2anc ⊢ ( 𝜑 → ( 𝑋 · ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
15 12 14 eqtrd ⊢ ( 𝜑 → ( 𝑋 · ( ( 𝑁 ‘ 𝑌 ) ( +g ‘ 𝑅 ) 𝑌 ) ) = ( 0g ‘ 𝑅 ) )
16 1 2 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
17 4 5 6 16 syl3anc ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
18 1 3 10 6 grpinvcld ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 )
19 1 2 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ∈ 𝐵 )
20 4 5 18 19 syl3anc ⊢ ( 𝜑 → ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ∈ 𝐵 )
21 1 7 8 3 grpinvid2 ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ∈ 𝐵 ) → ( ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ↔ ( ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ) = ( 0g ‘ 𝑅 ) ) )
22 10 17 20 21 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ↔ ( ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ) = ( 0g ‘ 𝑅 ) ) )
23 1 7 2 rngdi ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 · ( ( 𝑁 ‘ 𝑌 ) ( +g ‘ 𝑅 ) 𝑌 ) ) = ( ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ) )
24 23 eqcomd ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑁 ‘ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ) = ( 𝑋 · ( ( 𝑁 ‘ 𝑌 ) ( +g ‘ 𝑅 ) 𝑌 ) ) )
25 4 5 18 6 24 syl13anc ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ) = ( 𝑋 · ( ( 𝑁 ‘ 𝑌 ) ( +g ‘ 𝑅 ) 𝑌 ) ) )
26 25 eqeq1d ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ( +g ‘ 𝑅 ) ( 𝑋 · 𝑌 ) ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑋 · ( ( 𝑁 ‘ 𝑌 ) ( +g ‘ 𝑅 ) 𝑌 ) ) = ( 0g ‘ 𝑅 ) ) )
27 22 26 bitrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) ↔ ( 𝑋 · ( ( 𝑁 ‘ 𝑌 ) ( +g ‘ 𝑅 ) 𝑌 ) ) = ( 0g ‘ 𝑅 ) ) )
28 15 27 mpbird ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) = ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) )
29 28 eqcomd ⊢ ( 𝜑 → ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )