Metamath Proof Explorer

Theorem rngonegrmul

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

Ref Expression
Hypotheses ringnegmul.1 
|- G = ( 1st ` R )
ringnegmul.2 
|- H = ( 2nd ` R )
ringnegmul.3 
|- X = ran G
ringnegmul.4 
|- N = ( inv ` G )
Assertion rngonegrmul 
|- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` ( A H B ) ) = ( A H ( N ` B ) ) )

Proof

Step Hyp Ref Expression
1 ringnegmul.1 
 |-  G = ( 1st ` R )
2 ringnegmul.2 
 |-  H = ( 2nd ` R )
3 ringnegmul.3 
 |-  X = ran G
4 ringnegmul.4 
 |-  N = ( inv ` G )
5 1 rneqi 
 |-  ran G = ran ( 1st ` R )
6 3 5 eqtri 
 |-  X = ran ( 1st ` R )
7 eqid 
 |-  ( GId ` H ) = ( GId ` H )
8 6 2 7 rngo1cl 
 |-  ( R e. RingOps -> ( GId ` H ) e. X )
9 1 3 4 rngonegcl 
 |-  ( ( R e. RingOps /\ ( GId ` H ) e. X ) -> ( N ` ( GId ` H ) ) e. X )
10 8 9 mpdan 
 |-  ( R e. RingOps -> ( N ` ( GId ` H ) ) e. X )
11 1 2 3 rngoass 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ ( N ` ( GId ` H ) ) e. X ) ) -> ( ( A H B ) H ( N ` ( GId ` H ) ) ) = ( A H ( B H ( N ` ( GId ` H ) ) ) ) )
12 11 3exp2 
 |-  ( R e. RingOps -> ( A e. X -> ( B e. X -> ( ( N ` ( GId ` H ) ) e. X -> ( ( A H B ) H ( N ` ( GId ` H ) ) ) = ( A H ( B H ( N ` ( GId ` H ) ) ) ) ) ) ) )
13 12 com24 
 |-  ( R e. RingOps -> ( ( N ` ( GId ` H ) ) e. X -> ( B e. X -> ( A e. X -> ( ( A H B ) H ( N ` ( GId ` H ) ) ) = ( A H ( B H ( N ` ( GId ` H ) ) ) ) ) ) ) )
14 13 com34 
 |-  ( R e. RingOps -> ( ( N ` ( GId ` H ) ) e. X -> ( A e. X -> ( B e. X -> ( ( A H B ) H ( N ` ( GId ` H ) ) ) = ( A H ( B H ( N ` ( GId ` H ) ) ) ) ) ) ) )
15 10 14 mpd 
 |-  ( R e. RingOps -> ( A e. X -> ( B e. X -> ( ( A H B ) H ( N ` ( GId ` H ) ) ) = ( A H ( B H ( N ` ( GId ` H ) ) ) ) ) ) )
16 15 3imp 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( ( A H B ) H ( N ` ( GId ` H ) ) ) = ( A H ( B H ( N ` ( GId ` H ) ) ) ) )
17 1 2 3 rngocl 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A H B ) e. X )
18 17 3expb 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X ) ) -> ( A H B ) e. X )
19 1 2 3 4 7 rngonegmn1r 
 |-  ( ( R e. RingOps /\ ( A H B ) e. X ) -> ( N ` ( A H B ) ) = ( ( A H B ) H ( N ` ( GId ` H ) ) ) )
20 18 19 syldan 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X ) ) -> ( N ` ( A H B ) ) = ( ( A H B ) H ( N ` ( GId ` H ) ) ) )
21 20 3impb 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` ( A H B ) ) = ( ( A H B ) H ( N ` ( GId ` H ) ) ) )
22 1 2 3 4 7 rngonegmn1r 
 |-  ( ( R e. RingOps /\ B e. X ) -> ( N ` B ) = ( B H ( N ` ( GId ` H ) ) ) )
23 22 3adant2 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` B ) = ( B H ( N ` ( GId ` H ) ) ) )
24 23 oveq2d 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A H ( N ` B ) ) = ( A H ( B H ( N ` ( GId ` H ) ) ) ) )
25 16 21 24 3eqtr4d 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` ( A H B ) ) = ( A H ( N ` B ) ) )