Theorem idomcanr

Description: Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 13-Jul-2026)

	Ref	Expression
Hypotheses	isidom3.b	|- B = ( Base ` R )
	isidom3.t	|- .x. = ( .r ` R )
	isidom3.0	|- .0. = ( 0g ` R )
Assertion	idomcanr	|- ( ( ( R e. IDomn /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ Z =/= .0. ) -> ( ( X .x. Z ) = ( Y .x. Z ) -> X = Y ) )

Proof

Step	Hyp	Ref	Expression
1		isidom3.b	|- B = ( Base ` R )
2		isidom3.t	|- .x. = ( .r ` R )
3		isidom3.0	|- .0. = ( 0g ` R )
4		isidom	|- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
5	4	simplbi	|- ( R e. IDomn -> R e. CRing )
6	1 2	crngcom	|- ( ( R e. CRing /\ X e. B /\ Z e. B ) -> ( X .x. Z ) = ( Z .x. X ) )
7	6	3adant3r2	|- ( ( R e. CRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .x. Z ) = ( Z .x. X ) )
8	1 2	crngcom	|- ( ( R e. CRing /\ Y e. B /\ Z e. B ) -> ( Y .x. Z ) = ( Z .x. Y ) )
9	8	3adant3r1	|- ( ( R e. CRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( Y .x. Z ) = ( Z .x. Y ) )
10	7 9	eqeq12d	|- ( ( R e. CRing /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. Z ) = ( Y .x. Z ) <-> ( Z .x. X ) = ( Z .x. Y ) ) )
11	5 10	sylan	|- ( ( R e. IDomn /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .x. Z ) = ( Y .x. Z ) <-> ( Z .x. X ) = ( Z .x. Y ) ) )
12	11	adantr	|- ( ( ( R e. IDomn /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ Z =/= .0. ) -> ( ( X .x. Z ) = ( Y .x. Z ) <-> ( Z .x. X ) = ( Z .x. Y ) ) )
13		3anrot	|- ( ( Z e. B /\ X e. B /\ Y e. B ) <-> ( X e. B /\ Y e. B /\ Z e. B ) )
14	13	biimpri	|- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( Z e. B /\ X e. B /\ Y e. B ) )
15	1 2 3	idomcanl	|- ( ( ( R e. IDomn /\ ( Z e. B /\ X e. B /\ Y e. B ) ) /\ Z =/= .0. ) -> ( ( Z .x. X ) = ( Z .x. Y ) -> X = Y ) )
16	14 15	sylanl2	|- ( ( ( R e. IDomn /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ Z =/= .0. ) -> ( ( Z .x. X ) = ( Z .x. Y ) -> X = Y ) )
17	12 16	sylbid	|- ( ( ( R e. IDomn /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ Z =/= .0. ) -> ( ( X .x. Z ) = ( Y .x. Z ) -> X = Y ) )