Metamath Proof Explorer

Theorem ringmneg2

Description: Negation of a product in a ring. ( mulneg2 analog.) Compared with rngmneg2 , the proof is shorter making use of the existence of a ring unity. (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 ringmneg2 ( 𝜑 → ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )

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 5 6 13 14 syl13anc ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑋 · ( 𝑌 · ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) )
16 1 2 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
17 4 5 6 16 syl3anc ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
18 1 2 9 3 4 17 ringnegr ⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) · ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )
19 1 2 9 3 4 6 ringnegr ⊢ ( 𝜑 → ( 𝑌 · ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) = ( 𝑁 ‘ 𝑌 ) )
20 19 oveq2d ⊢ ( 𝜑 → ( 𝑋 · ( 𝑌 · ( 𝑁 ‘ ( 1r ‘ 𝑅 ) ) ) ) = ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) )
21 15 18 20 3eqtr3rd ⊢ ( 𝜑 → ( 𝑋 · ( 𝑁 ‘ 𝑌 ) ) = ( 𝑁 ‘ ( 𝑋 · 𝑌 ) ) )