Metamath Proof Explorer


Theorem dmnnzd

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

Ref Expression
Hypotheses dmnnzd.1 G=1stR
dmnnzd.2 H=2ndR
dmnnzd.3 X=ranG
dmnnzd.4 Z=GIdG
Assertion dmnnzd RDmnAXBXAHB=ZA=ZB=Z

Proof

Step Hyp Ref Expression
1 dmnnzd.1 G=1stR
2 dmnnzd.2 H=2ndR
3 dmnnzd.3 X=ranG
4 dmnnzd.4 Z=GIdG
5 eqid GIdH=GIdH
6 1 2 3 4 5 isdmn3 RDmnRCRingOpsGIdHZaXbXaHb=Za=Zb=Z
7 6 simp3bi RDmnaXbXaHb=Za=Zb=Z
8 oveq1 a=AaHb=AHb
9 8 eqeq1d a=AaHb=ZAHb=Z
10 eqeq1 a=Aa=ZA=Z
11 10 orbi1d a=Aa=Zb=ZA=Zb=Z
12 9 11 imbi12d a=AaHb=Za=Zb=ZAHb=ZA=Zb=Z
13 oveq2 b=BAHb=AHB
14 13 eqeq1d b=BAHb=ZAHB=Z
15 eqeq1 b=Bb=ZB=Z
16 15 orbi2d b=BA=Zb=ZA=ZB=Z
17 14 16 imbi12d b=BAHb=ZA=Zb=ZAHB=ZA=ZB=Z
18 12 17 rspc2v AXBXaXbXaHb=Za=Zb=ZAHB=ZA=ZB=Z
19 7 18 syl5com RDmnAXBXAHB=ZA=ZB=Z
20 19 expd RDmnAXBXAHB=ZA=ZB=Z
21 20 3imp2 RDmnAXBXAHB=ZA=ZB=Z