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

Metamath Proof Explorer

Theorem dmncan1

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 dmncan1 
|- ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A =/= Z ) -> ( ( A H B ) = ( A H C ) -> B = C ) )

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 dmnrngo 
 |-  ( R e. Dmn -> R e. RingOps )
6 eqid 
 |-  ( /g ` G ) = ( /g ` G )
7 1 2 3 6 rngosubdi 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H ( B ( /g ` G ) C ) ) = ( ( A H B ) ( /g ` G ) ( A H C ) ) )
8 5 7 sylan 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H ( B ( /g ` G ) C ) ) = ( ( A H B ) ( /g ` G ) ( A H C ) ) )
9 8 adantr 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A =/= Z ) -> ( A H ( B ( /g ` G ) C ) ) = ( ( A H B ) ( /g ` G ) ( A H C ) ) )
10 9 eqeq1d 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A =/= Z ) -> ( ( A H ( B ( /g ` G ) C ) ) = Z <-> ( ( A H B ) ( /g ` G ) ( A H C ) ) = Z ) )
11 1 rngogrpo 
 |-  ( R e. RingOps -> G e. GrpOp )
12 5 11 syl 
 |-  ( R e. Dmn -> G e. GrpOp )
13 3 6 grpodivcl 
 |-  ( ( G e. GrpOp /\ B e. X /\ C e. X ) -> ( B ( /g ` G ) C ) e. X )
14 13 3expb 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> ( B ( /g ` G ) C ) e. X )
15 12 14 sylan 
 |-  ( ( R e. Dmn /\ ( B e. X /\ C e. X ) ) -> ( B ( /g ` G ) C ) e. X )
16 15 adantlr 
 |-  ( ( ( R e. Dmn /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( B ( /g ` G ) C ) e. X )
17 1 2 3 4 dmnnzd 
 |-  ( ( R e. Dmn /\ ( A e. X /\ ( B ( /g ` G ) C ) e. X /\ ( A H ( B ( /g ` G ) C ) ) = Z ) ) -> ( A = Z \/ ( B ( /g ` G ) C ) = Z ) )
18 17 3exp2 
 |-  ( R e. Dmn -> ( A e. X -> ( ( B ( /g ` G ) C ) e. X -> ( ( A H ( B ( /g ` G ) C ) ) = Z -> ( A = Z \/ ( B ( /g ` G ) C ) = Z ) ) ) ) )
19 18 imp31 
 |-  ( ( ( R e. Dmn /\ A e. X ) /\ ( B ( /g ` G ) C ) e. X ) -> ( ( A H ( B ( /g ` G ) C ) ) = Z -> ( A = Z \/ ( B ( /g ` G ) C ) = Z ) ) )
20 16 19 syldan 
 |-  ( ( ( R e. Dmn /\ A e. X ) /\ ( B e. X /\ C e. X ) ) -> ( ( A H ( B ( /g ` G ) C ) ) = Z -> ( A = Z \/ ( B ( /g ` G ) C ) = Z ) ) )
21 20 exp43 
 |-  ( R e. Dmn -> ( A e. X -> ( B e. X -> ( C e. X -> ( ( A H ( B ( /g ` G ) C ) ) = Z -> ( A = Z \/ ( B ( /g ` G ) C ) = Z ) ) ) ) ) )
22 21 3imp2 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H ( B ( /g ` G ) C ) ) = Z -> ( A = Z \/ ( B ( /g ` G ) C ) = Z ) ) )
23 neor 
 |-  ( ( A = Z \/ ( B ( /g ` G ) C ) = Z ) <-> ( A =/= Z -> ( B ( /g ` G ) C ) = Z ) )
24 22 23 imbitrdi 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H ( B ( /g ` G ) C ) ) = Z -> ( A =/= Z -> ( B ( /g ` G ) C ) = Z ) ) )
25 24 com23 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A =/= Z -> ( ( A H ( B ( /g ` G ) C ) ) = Z -> ( B ( /g ` G ) C ) = Z ) ) )
26 25 imp 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A =/= Z ) -> ( ( A H ( B ( /g ` G ) C ) ) = Z -> ( B ( /g ` G ) C ) = Z ) )
27 10 26 sylbird 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A =/= Z ) -> ( ( ( A H B ) ( /g ` G ) ( A H C ) ) = Z -> ( B ( /g ` G ) C ) = Z ) )
28 12 adantr 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> G e. GrpOp )
29 1 2 3 rngocl 
 |-  ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A H B ) e. X )
30 29 3adant3r3 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H B ) e. X )
31 5 30 sylan 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H B ) e. X )
32 1 2 3 rngocl 
 |-  ( ( R e. RingOps /\ A e. X /\ C e. X ) -> ( A H C ) e. X )
33 32 3adant3r2 
 |-  ( ( R e. RingOps /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H C ) e. X )
34 5 33 sylan 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A H C ) e. X )
35 3 4 6 grpoeqdivid 
 |-  ( ( G e. GrpOp /\ ( A H B ) e. X /\ ( A H C ) e. X ) -> ( ( A H B ) = ( A H C ) <-> ( ( A H B ) ( /g ` G ) ( A H C ) ) = Z ) )
36 28 31 34 35 syl3anc 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A H B ) = ( A H C ) <-> ( ( A H B ) ( /g ` G ) ( A H C ) ) = Z ) )
37 36 adantr 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A =/= Z ) -> ( ( A H B ) = ( A H C ) <-> ( ( A H B ) ( /g ` G ) ( A H C ) ) = Z ) )
38 3 4 6 grpoeqdivid 
 |-  ( ( G e. GrpOp /\ B e. X /\ C e. X ) -> ( B = C <-> ( B ( /g ` G ) C ) = Z ) )
39 38 3expb 
 |-  ( ( G e. GrpOp /\ ( B e. X /\ C e. X ) ) -> ( B = C <-> ( B ( /g ` G ) C ) = Z ) )
40 12 39 sylan 
 |-  ( ( R e. Dmn /\ ( B e. X /\ C e. X ) ) -> ( B = C <-> ( B ( /g ` G ) C ) = Z ) )
41 40 3adantr1 
 |-  ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B = C <-> ( B ( /g ` G ) C ) = Z ) )
42 41 adantr 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A =/= Z ) -> ( B = C <-> ( B ( /g ` G ) C ) = Z ) )
43 27 37 42 3imtr4d 
 |-  ( ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ C e. X ) ) /\ A =/= Z ) -> ( ( A H B ) = ( A H C ) -> B = C ) )