# Metamath Proof Explorer

## Theorem divrngcl

Description: The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010)

Ref Expression
Hypotheses isdivrng1.1 ${⊢}{G}={1}^{st}\left({R}\right)$
isdivrng1.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
isdivrng1.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
isdivrng1.4 ${⊢}{X}=\mathrm{ran}{G}$
Assertion divrngcl ${⊢}\left({R}\in \mathrm{DivRingOps}\wedge {A}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\to {A}{H}{B}\in \left({X}\setminus \left\{{Z}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 isdivrng1.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 isdivrng1.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 isdivrng1.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
4 isdivrng1.4 ${⊢}{X}=\mathrm{ran}{G}$
5 1 2 3 4 isdrngo1 ${⊢}{R}\in \mathrm{DivRingOps}↔\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)$
6 ovres ${⊢}\left({A}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\to {A}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right){B}={A}{H}{B}$
7 6 adantl ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\wedge \left({A}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\right)\to {A}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right){B}={A}{H}{B}$
8 eqid ${⊢}\mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)=\mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)$
9 8 grpocl ${⊢}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\wedge {A}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\wedge {B}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\right)\to {A}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right){B}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)$
10 9 3expib ${⊢}{{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\to \left(\left({A}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\wedge {B}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\right)\to {A}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right){B}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\right)$
11 10 adantl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \left(\left({A}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\wedge {B}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\right)\to {A}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right){B}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\right)$
12 grporndm ${⊢}{{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\to \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)=\mathrm{dom}\mathrm{dom}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)$
13 12 adantl ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)=\mathrm{dom}\mathrm{dom}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)$
14 difss ${⊢}{X}\setminus \left\{{Z}\right\}\subseteq {X}$
15 xpss12 ${⊢}\left({X}\setminus \left\{{Z}\right\}\subseteq {X}\wedge {X}\setminus \left\{{Z}\right\}\subseteq {X}\right)\to \left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\subseteq {X}×{X}$
16 14 14 15 mp2an ${⊢}\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\subseteq {X}×{X}$
17 1 2 4 rngosm ${⊢}{R}\in \mathrm{RingOps}\to {H}:{X}×{X}⟶{X}$
18 17 fdmd ${⊢}{R}\in \mathrm{RingOps}\to \mathrm{dom}{H}={X}×{X}$
19 16 18 sseqtrrid ${⊢}{R}\in \mathrm{RingOps}\to \left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\subseteq \mathrm{dom}{H}$
20 ssdmres ${⊢}\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\subseteq \mathrm{dom}{H}↔\mathrm{dom}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)=\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)$
21 19 20 sylib ${⊢}{R}\in \mathrm{RingOps}\to \mathrm{dom}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)=\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)$
22 21 adantr ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \mathrm{dom}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)=\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)$
23 22 dmeqd ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \mathrm{dom}\mathrm{dom}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)=\mathrm{dom}\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)$
24 dmxpid ${⊢}\mathrm{dom}\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)={X}\setminus \left\{{Z}\right\}$
25 23 24 syl6eq ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \mathrm{dom}\mathrm{dom}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)={X}\setminus \left\{{Z}\right\}$
26 13 25 eqtrd ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)={X}\setminus \left\{{Z}\right\}$
27 26 eleq2d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \left({A}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)↔{A}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)$
28 26 eleq2d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \left({B}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)↔{B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)$
29 27 28 anbi12d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \left(\left({A}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\wedge {B}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)\right)↔\left({A}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\right)$
30 26 eleq2d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \left({A}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right){B}\in \mathrm{ran}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right)↔{A}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right){B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)$
31 11 29 30 3imtr3d ${⊢}\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\to \left(\left({A}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\to {A}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right){B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)$
32 31 imp ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\wedge \left({A}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\right)\to {A}\left({{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\right){B}\in \left({X}\setminus \left\{{Z}\right\}\right)$
33 7 32 eqeltrrd ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\wedge \left({A}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\right)\to {A}{H}{B}\in \left({X}\setminus \left\{{Z}\right\}\right)$
34 33 3impb ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {{H}↾}_{\left(\left({X}\setminus \left\{{Z}\right\}\right)×\left({X}\setminus \left\{{Z}\right\}\right)\right)}\in \mathrm{GrpOp}\right)\wedge {A}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\to {A}{H}{B}\in \left({X}\setminus \left\{{Z}\right\}\right)$
35 5 34 syl3an1b ${⊢}\left({R}\in \mathrm{DivRingOps}\wedge {A}\in \left({X}\setminus \left\{{Z}\right\}\right)\wedge {B}\in \left({X}\setminus \left\{{Z}\right\}\right)\right)\to {A}{H}{B}\in \left({X}\setminus \left\{{Z}\right\}\right)$