Metamath Proof Explorer


Theorem rngoneglmul

Description: Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses ringnegmul.1 𝐺 = ( 1st𝑅 )
ringnegmul.2 𝐻 = ( 2nd𝑅 )
ringnegmul.3 𝑋 = ran 𝐺
ringnegmul.4 𝑁 = ( inv ‘ 𝐺 )
Assertion rngoneglmul ( ( 𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝑁𝐴 ) 𝐻 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ringnegmul.1 𝐺 = ( 1st𝑅 )
2 ringnegmul.2 𝐻 = ( 2nd𝑅 )
3 ringnegmul.3 𝑋 = ran 𝐺
4 ringnegmul.4 𝑁 = ( inv ‘ 𝐺 )
5 1 rneqi ran 𝐺 = ran ( 1st𝑅 )
6 3 5 eqtri 𝑋 = ran ( 1st𝑅 )
7 eqid ( GId ‘ 𝐻 ) = ( GId ‘ 𝐻 )
8 6 2 7 rngo1cl ( 𝑅 ∈ RingOps → ( GId ‘ 𝐻 ) ∈ 𝑋 )
9 1 3 4 rngonegcl ( ( 𝑅 ∈ RingOps ∧ ( GId ‘ 𝐻 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋 )
10 8 9 mpdan ( 𝑅 ∈ RingOps → ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋 )
11 1 2 3 rngoass ( ( 𝑅 ∈ RingOps ∧ ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋𝐴𝑋𝐵𝑋 ) ) → ( ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 𝐴 ) 𝐻 𝐵 ) = ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 ( 𝐴 𝐻 𝐵 ) ) )
12 11 3exp2 ( 𝑅 ∈ RingOps → ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋 → ( 𝐴𝑋 → ( 𝐵𝑋 → ( ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 𝐴 ) 𝐻 𝐵 ) = ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 ( 𝐴 𝐻 𝐵 ) ) ) ) ) )
13 10 12 mpd ( 𝑅 ∈ RingOps → ( 𝐴𝑋 → ( 𝐵𝑋 → ( ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 𝐴 ) 𝐻 𝐵 ) = ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 ( 𝐴 𝐻 𝐵 ) ) ) ) )
14 13 3imp ( ( 𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋 ) → ( ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 𝐴 ) 𝐻 𝐵 ) = ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 ( 𝐴 𝐻 𝐵 ) ) )
15 1 2 3 4 7 rngonegmn1l ( ( 𝑅 ∈ RingOps ∧ 𝐴𝑋 ) → ( 𝑁𝐴 ) = ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 𝐴 ) )
16 15 3adant3 ( ( 𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁𝐴 ) = ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 𝐴 ) )
17 16 oveq1d ( ( 𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋 ) → ( ( 𝑁𝐴 ) 𝐻 𝐵 ) = ( ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 𝐴 ) 𝐻 𝐵 ) )
18 1 2 3 rngocl ( ( 𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
19 18 3expb ( ( 𝑅 ∈ RingOps ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
20 1 2 3 4 7 rngonegmn1l ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 ( 𝐴 𝐻 𝐵 ) ) )
21 19 20 syldan ( ( 𝑅 ∈ RingOps ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 ( 𝐴 𝐻 𝐵 ) ) )
22 21 3impb ( ( 𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) 𝐻 ( 𝐴 𝐻 𝐵 ) ) )
23 14 17 22 3eqtr4rd ( ( 𝑅 ∈ RingOps ∧ 𝐴𝑋𝐵𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝑁𝐴 ) 𝐻 𝐵 ) )