Metamath Proof Explorer


Theorem ringmneg1

Description: Negation of a product in a ring. ( mulneg1 analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)

Ref Expression
Hypotheses ringneglmul.b 𝐵 = ( Base ‘ 𝑅 )
ringneglmul.t · = ( .r𝑅 )
ringneglmul.n 𝑁 = ( invg𝑅 )
ringneglmul.r ( 𝜑𝑅 ∈ Ring )
ringneglmul.x ( 𝜑𝑋𝐵 )
ringneglmul.y ( 𝜑𝑌𝐵 )
Assertion ringmneg1 ( 𝜑 → ( ( 𝑁𝑋 ) · 𝑌 ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )

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 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
8 4 7 syl ( 𝜑𝑅 ∈ Grp )
9 eqid ( 1r𝑅 ) = ( 1r𝑅 )
10 1 9 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ 𝐵 )
11 4 10 syl ( 𝜑 → ( 1r𝑅 ) ∈ 𝐵 )
12 1 3 grpinvcl ( ( 𝑅 ∈ Grp ∧ ( 1r𝑅 ) ∈ 𝐵 ) → ( 𝑁 ‘ ( 1r𝑅 ) ) ∈ 𝐵 )
13 8 11 12 syl2anc ( 𝜑 → ( 𝑁 ‘ ( 1r𝑅 ) ) ∈ 𝐵 )
14 1 2 ringass ( ( 𝑅 ∈ Ring ∧ ( ( 𝑁 ‘ ( 1r𝑅 ) ) ∈ 𝐵𝑋𝐵𝑌𝐵 ) ) → ( ( ( 𝑁 ‘ ( 1r𝑅 ) ) · 𝑋 ) · 𝑌 ) = ( ( 𝑁 ‘ ( 1r𝑅 ) ) · ( 𝑋 · 𝑌 ) ) )
15 4 13 5 6 14 syl13anc ( 𝜑 → ( ( ( 𝑁 ‘ ( 1r𝑅 ) ) · 𝑋 ) · 𝑌 ) = ( ( 𝑁 ‘ ( 1r𝑅 ) ) · ( 𝑋 · 𝑌 ) ) )
16 1 2 9 3 4 5 ringnegl ( 𝜑 → ( ( 𝑁 ‘ ( 1r𝑅 ) ) · 𝑋 ) = ( 𝑁𝑋 ) )
17 16 oveq1d ( 𝜑 → ( ( ( 𝑁 ‘ ( 1r𝑅 ) ) · 𝑋 ) · 𝑌 ) = ( ( 𝑁𝑋 ) · 𝑌 ) )
18 1 2 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
19 4 5 6 18 syl3anc ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
20 1 2 9 3 4 19 ringnegl ( 𝜑 → ( ( 𝑁 ‘ ( 1r𝑅 ) ) · ( 𝑋 · 𝑌 ) ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )
21 15 17 20 3eqtr3d ( 𝜑 → ( ( 𝑁𝑋 ) · 𝑌 ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )