This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dmncan2

Description: Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011)

Ref Expression
Hypotheses dmncan.1 
|- G = ( 1st ` R )
dmncan.2 
|- H = ( 2nd ` R )
dmncan.3 
|- X = ran G
dmncan.4 
|- Z = ( GId ` G )
Assertion dmncan2 
|- ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ C =/= Z ) -> ( ( A H C ) = ( B H C ) -> A = B ) )

Proof

Step Hyp Ref Expression
1 dmncan.1 
 |-  G = ( 1st ` R )
2 dmncan.2 
 |-  H = ( 2nd ` R )
3 dmncan.3 
 |-  X = ran G
4 dmncan.4 
 |-  Z = ( GId ` G )
5 dmncrng 
 |-  ( R e. Dmn -> R e. CRingOps )
6 1 2 3 crngocom 
 |-  ( ( R e. CRingOps /\ A e. X /\ C e. X ) -> ( A H C ) = ( C H A ) )
7 6 3adant3r2 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H C ) = ( C H A ) )
8 1 2 3 crngocom 
 |-  ( ( R e. CRingOps /\ B e. X /\ C e. X ) -> ( B H C ) = ( C H B ) )
9 8 3adant3r1 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B H C ) = ( C H B ) )
10 7 9 eqeq12d 
 |-  ( ( R e. CRingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H C ) = ( B H C ) <-> ( C H A ) = ( C H B ) ) )
11 5 10 sylan 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H C ) = ( B H C ) <-> ( C H A ) = ( C H B ) ) )
12 11 adantr 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ C =/= Z ) -> ( ( A H C ) = ( B H C ) <-> ( C H A ) = ( C H B ) ) )
13 3anrot 
 |-  ( ( C e. X /\ A e. X /\ B e. X ) <-> ( A e. X /\ B e. X /\ C e. X ) )
14 13 biimpri 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> ( C e. X /\ A e. X /\ B e. X ) )
15 1 2 3 4 dmncan1 
 |-  ( ( ( R e. Dmn /\ ( C e. X /\ A e. X /\ B e. X ) ) /\ C =/= Z ) -> ( ( C H A ) = ( C H B ) -> A = B ) )
16 14 15 sylanl2 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ C =/= Z ) -> ( ( C H A ) = ( C H B ) -> A = B ) )
17 12 16 sylbid 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ C =/= Z ) -> ( ( A H C ) = ( B H C ) -> A = B ) )