Theorem dmnnzd

Description: A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010)

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

Proof

Step	Hyp	Ref	Expression
1		dmnnzd.1	|- G = ( 1st ` R )
2		dmnnzd.2	|- H = ( 2nd ` R )
3		dmnnzd.3	|- X = ran G
4		dmnnzd.4	|- Z = ( GId ` G )
5		eqid	|- ( GId ` H ) = ( GId ` H )
6	1 2 3 4 5	isdmn3	|- ( R e. Dmn <-> ( R e. CRingOps /\ ( GId ` H ) =/= Z /\ A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) ) )
7	6	simp3bi	|- ( R e. Dmn -> A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) )
8		oveq1	|- ( a = A -> ( a H b ) = ( A H b ) )
9	8	eqeq1d	|- ( a = A -> ( ( a H b ) = Z <-> ( A H b ) = Z ) )
10		eqeq1	|- ( a = A -> ( a = Z <-> A = Z ) )
11	10	orbi1d	|- ( a = A -> ( ( a = Z \/ b = Z ) <-> ( A = Z \/ b = Z ) ) )
12	9 11	imbi12d	|- ( a = A -> ( ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) <-> ( ( A H b ) = Z -> ( A = Z \/ b = Z ) ) ) )
13		oveq2	|- ( b = B -> ( A H b ) = ( A H B ) )
14	13	eqeq1d	|- ( b = B -> ( ( A H b ) = Z <-> ( A H B ) = Z ) )
15		eqeq1	|- ( b = B -> ( b = Z <-> B = Z ) )
16	15	orbi2d	|- ( b = B -> ( ( A = Z \/ b = Z ) <-> ( A = Z \/ B = Z ) ) )
17	14 16	imbi12d	|- ( b = B -> ( ( ( A H b ) = Z -> ( A = Z \/ b = Z ) ) <-> ( ( A H B ) = Z -> ( A = Z \/ B = Z ) ) ) )
18	12 17	rspc2v	|- ( ( A e. X /\ B e. X ) -> ( A. a e. X A. b e. X ( ( a H b ) = Z -> ( a = Z \/ b = Z ) ) -> ( ( A H B ) = Z -> ( A = Z \/ B = Z ) ) ) )
19	7 18	syl5com	|- ( R e. Dmn -> ( ( A e. X /\ B e. X ) -> ( ( A H B ) = Z -> ( A = Z \/ B = Z ) ) ) )
20	19	expd	|- ( R e. Dmn -> ( A e. X -> ( B e. X -> ( ( A H B ) = Z -> ( A = Z \/ B = Z ) ) ) ) )
21	20	3imp2	|- ( ( R e. Dmn /\ ( A e. X /\ B e. X /\ ( A H B ) = Z ) ) -> ( A = Z \/ B = Z ) )