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 
|- G = ( 1st ` R )
ringnegmul.2 
|- H = ( 2nd ` R )
ringnegmul.3 
|- X = ran G
ringnegmul.4 
|- N = ( inv ` G )
Assertion rngoneglmul 
|- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` ( A H B ) ) = ( ( N ` A ) H 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 /\ ( ( N ` ( GId ` H ) ) e. X /\ A e. X /\ B e. X ) ) -> ( ( ( N ` ( GId ` H ) ) H A ) H B ) = ( ( N ` ( GId ` H ) ) H ( A H B ) ) )
12 11 3exp2 
 |-  ( R e. RingOps -> ( ( N ` ( GId ` H ) ) e. X -> ( A e. X -> ( B e. X -> ( ( ( N ` ( GId ` H ) ) H A ) H B ) = ( ( N ` ( GId ` H ) ) H ( A H B ) ) ) ) ) )
13 10 12 mpd 
 |-  ( R e. RingOps -> ( A e. X -> ( B e. X -> ( ( ( N ` ( GId ` H ) ) H A ) H B ) = ( ( N ` ( GId ` H ) ) H ( A H B ) ) ) ) )
14 13 3imp 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( ( ( N ` ( GId ` H ) ) H A ) H B ) = ( ( N ` ( GId ` H ) ) H ( A H B ) ) )
15 1 2 3 4 7 rngonegmn1l 
 |-  ( ( R e. RingOps /\ A e. X ) -> ( N ` A ) = ( ( N ` ( GId ` H ) ) H A ) )
16 15 3adant3 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` A ) = ( ( N ` ( GId ` H ) ) H A ) )
17 16 oveq1d 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( ( N ` A ) H B ) = ( ( ( N ` ( GId ` H ) ) H A ) H B ) )
18 1 2 3 rngocl 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A H B ) e. X )
19 18 3expb 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X ) ) -> ( A H B ) e. X )
20 1 2 3 4 7 rngonegmn1l 
 |-  ( ( R e. RingOps /\ ( A H B ) e. X ) -> ( N ` ( A H B ) ) = ( ( N ` ( GId ` H ) ) H ( A H B ) ) )
21 19 20 syldan 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X ) ) -> ( N ` ( A H B ) ) = ( ( N ` ( GId ` H ) ) H ( A H B ) ) )
22 21 3impb 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` ( A H B ) ) = ( ( N ` ( GId ` H ) ) H ( A H B ) ) )
23 14 17 22 3eqtr4rd 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( N ` ( A H B ) ) = ( ( N ` A ) H B ) )