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 ) )