# Metamath Proof Explorer

## Theorem zerdivemp1x

Description: In a unitary ring a left invertible element is not a zero divisor. See also ringinvnzdiv . (Contributed by Jeff Madsen, 18-Apr-2010)

Ref Expression
Hypotheses zerdivempx.1 ${⊢}{G}={1}^{st}\left({R}\right)$
zerdivempx.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
zerdivempx.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
zerdivempx.4 ${⊢}{X}=\mathrm{ran}{G}$
zerdivempx.5 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
Assertion zerdivemp1x ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge \exists {a}\in {X}\phantom{\rule{.4em}{0ex}}{a}{H}{A}={U}\right)\to \left({B}\in {X}\to \left({A}{H}{B}={Z}\to {B}={Z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 zerdivempx.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 zerdivempx.2 ${⊢}{H}={2}^{nd}\left({R}\right)$
3 zerdivempx.3 ${⊢}{Z}=\mathrm{GId}\left({G}\right)$
4 zerdivempx.4 ${⊢}{X}=\mathrm{ran}{G}$
5 zerdivempx.5 ${⊢}{U}=\mathrm{GId}\left({H}\right)$
6 oveq2 ${⊢}{A}{H}{B}={Z}\to {a}{H}\left({A}{H}{B}\right)={a}{H}{Z}$
7 simpl1 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\wedge {B}\in {X}\right)\wedge \left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\right)\to {R}\in \mathrm{RingOps}$
8 simpr1 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\wedge {B}\in {X}\right)\wedge \left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\right)\to {a}\in {X}$
9 simpr3 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\wedge {B}\in {X}\right)\wedge \left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\right)\to {A}\in {X}$
10 simpl3 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\wedge {B}\in {X}\right)\wedge \left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\right)\to {B}\in {X}$
11 1 2 4 rngoass ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({a}\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)\right)\to \left({a}{H}{A}\right){H}{B}={a}{H}\left({A}{H}{B}\right)$
12 7 8 9 10 11 syl13anc ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\wedge {B}\in {X}\right)\wedge \left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\right)\to \left({a}{H}{A}\right){H}{B}={a}{H}\left({A}{H}{B}\right)$
13 eqtr ${⊢}\left(\left({a}{H}{A}\right){H}{B}={a}{H}\left({A}{H}{B}\right)\wedge {a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\right)\to \left({a}{H}{A}\right){H}{B}={a}{H}{Z}$
14 13 ex ${⊢}\left({a}{H}{A}\right){H}{B}={a}{H}\left({A}{H}{B}\right)\to \left({a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\to \left({a}{H}{A}\right){H}{B}={a}{H}{Z}\right)$
15 eqtr ${⊢}\left({U}{H}{B}=\left({a}{H}{A}\right){H}{B}\wedge \left({a}{H}{A}\right){H}{B}={a}{H}{Z}\right)\to {U}{H}{B}={a}{H}{Z}$
16 3 4 1 2 rngorz ${⊢}\left({R}\in \mathrm{RingOps}\wedge {a}\in {X}\right)\to {a}{H}{Z}={Z}$
17 16 3adant3 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {a}\in {X}\wedge {B}\in {X}\right)\to {a}{H}{Z}={Z}$
18 1 rneqi ${⊢}\mathrm{ran}{G}=\mathrm{ran}{1}^{st}\left({R}\right)$
19 4 18 eqtri ${⊢}{X}=\mathrm{ran}{1}^{st}\left({R}\right)$
20 2 19 5 rngolidm ${⊢}\left({R}\in \mathrm{RingOps}\wedge {B}\in {X}\right)\to {U}{H}{B}={B}$
21 20 3adant2 ${⊢}\left({R}\in \mathrm{RingOps}\wedge {a}\in {X}\wedge {B}\in {X}\right)\to {U}{H}{B}={B}$
22 simp1 ${⊢}\left({U}{H}{B}={a}{H}{Z}\wedge {U}{H}{B}={B}\wedge {a}{H}{Z}={Z}\right)\to {U}{H}{B}={a}{H}{Z}$
23 simp2 ${⊢}\left({U}{H}{B}={a}{H}{Z}\wedge {U}{H}{B}={B}\wedge {a}{H}{Z}={Z}\right)\to {U}{H}{B}={B}$
24 simp3 ${⊢}\left({U}{H}{B}={a}{H}{Z}\wedge {U}{H}{B}={B}\wedge {a}{H}{Z}={Z}\right)\to {a}{H}{Z}={Z}$
25 22 23 24 3eqtr3d ${⊢}\left({U}{H}{B}={a}{H}{Z}\wedge {U}{H}{B}={B}\wedge {a}{H}{Z}={Z}\right)\to {B}={Z}$
26 25 a1d ${⊢}\left({U}{H}{B}={a}{H}{Z}\wedge {U}{H}{B}={B}\wedge {a}{H}{Z}={Z}\right)\to \left({A}\in {X}\to {B}={Z}\right)$
27 26 3exp ${⊢}{U}{H}{B}={a}{H}{Z}\to \left({U}{H}{B}={B}\to \left({a}{H}{Z}={Z}\to \left({A}\in {X}\to {B}={Z}\right)\right)\right)$
28 27 com14 ${⊢}{A}\in {X}\to \left({U}{H}{B}={B}\to \left({a}{H}{Z}={Z}\to \left({U}{H}{B}={a}{H}{Z}\to {B}={Z}\right)\right)\right)$
29 28 com13 ${⊢}{a}{H}{Z}={Z}\to \left({U}{H}{B}={B}\to \left({A}\in {X}\to \left({U}{H}{B}={a}{H}{Z}\to {B}={Z}\right)\right)\right)$
30 17 21 29 sylc ${⊢}\left({R}\in \mathrm{RingOps}\wedge {a}\in {X}\wedge {B}\in {X}\right)\to \left({A}\in {X}\to \left({U}{H}{B}={a}{H}{Z}\to {B}={Z}\right)\right)$
31 30 3exp ${⊢}{R}\in \mathrm{RingOps}\to \left({a}\in {X}\to \left({B}\in {X}\to \left({A}\in {X}\to \left({U}{H}{B}={a}{H}{Z}\to {B}={Z}\right)\right)\right)\right)$
32 31 com15 ${⊢}{U}{H}{B}={a}{H}{Z}\to \left({a}\in {X}\to \left({B}\in {X}\to \left({A}\in {X}\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)\right)$
33 32 com24 ${⊢}{U}{H}{B}={a}{H}{Z}\to \left({A}\in {X}\to \left({B}\in {X}\to \left({a}\in {X}\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)\right)$
34 15 33 syl ${⊢}\left({U}{H}{B}=\left({a}{H}{A}\right){H}{B}\wedge \left({a}{H}{A}\right){H}{B}={a}{H}{Z}\right)\to \left({A}\in {X}\to \left({B}\in {X}\to \left({a}\in {X}\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)\right)$
35 34 ex ${⊢}{U}{H}{B}=\left({a}{H}{A}\right){H}{B}\to \left(\left({a}{H}{A}\right){H}{B}={a}{H}{Z}\to \left({A}\in {X}\to \left({B}\in {X}\to \left({a}\in {X}\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)\right)\right)$
36 35 eqcoms ${⊢}\left({a}{H}{A}\right){H}{B}={U}{H}{B}\to \left(\left({a}{H}{A}\right){H}{B}={a}{H}{Z}\to \left({A}\in {X}\to \left({B}\in {X}\to \left({a}\in {X}\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)\right)\right)$
37 36 com25 ${⊢}\left({a}{H}{A}\right){H}{B}={U}{H}{B}\to \left({a}\in {X}\to \left({A}\in {X}\to \left({B}\in {X}\to \left(\left({a}{H}{A}\right){H}{B}={a}{H}{Z}\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)\right)\right)$
38 oveq1 ${⊢}{a}{H}{A}={U}\to \left({a}{H}{A}\right){H}{B}={U}{H}{B}$
39 37 38 syl11 ${⊢}{a}\in {X}\to \left({a}{H}{A}={U}\to \left({A}\in {X}\to \left({B}\in {X}\to \left(\left({a}{H}{A}\right){H}{B}={a}{H}{Z}\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)\right)\right)$
40 39 3imp ${⊢}\left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\to \left({B}\in {X}\to \left(\left({a}{H}{A}\right){H}{B}={a}{H}{Z}\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)$
41 40 com13 ${⊢}\left({a}{H}{A}\right){H}{B}={a}{H}{Z}\to \left({B}\in {X}\to \left(\left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)$
42 14 41 syl6 ${⊢}\left({a}{H}{A}\right){H}{B}={a}{H}\left({A}{H}{B}\right)\to \left({a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\to \left({B}\in {X}\to \left(\left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\to \left({R}\in \mathrm{RingOps}\to {B}={Z}\right)\right)\right)\right)$
43 42 com15 ${⊢}{R}\in \mathrm{RingOps}\to \left({a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\to \left({B}\in {X}\to \left(\left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\to \left(\left({a}{H}{A}\right){H}{B}={a}{H}\left({A}{H}{B}\right)\to {B}={Z}\right)\right)\right)\right)$
44 43 3imp1 ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\wedge {B}\in {X}\right)\wedge \left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\right)\to \left(\left({a}{H}{A}\right){H}{B}={a}{H}\left({A}{H}{B}\right)\to {B}={Z}\right)$
45 12 44 mpd ${⊢}\left(\left({R}\in \mathrm{RingOps}\wedge {a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\wedge {B}\in {X}\right)\wedge \left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\right)\to {B}={Z}$
46 45 3exp1 ${⊢}{R}\in \mathrm{RingOps}\to \left({a}{H}\left({A}{H}{B}\right)={a}{H}{Z}\to \left({B}\in {X}\to \left(\left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\to {B}={Z}\right)\right)\right)$
47 6 46 syl5com ${⊢}{A}{H}{B}={Z}\to \left({R}\in \mathrm{RingOps}\to \left({B}\in {X}\to \left(\left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\to {B}={Z}\right)\right)\right)$
48 47 com14 ${⊢}\left({a}\in {X}\wedge {a}{H}{A}={U}\wedge {A}\in {X}\right)\to \left({R}\in \mathrm{RingOps}\to \left({B}\in {X}\to \left({A}{H}{B}={Z}\to {B}={Z}\right)\right)\right)$
49 48 3exp ${⊢}{a}\in {X}\to \left({a}{H}{A}={U}\to \left({A}\in {X}\to \left({R}\in \mathrm{RingOps}\to \left({B}\in {X}\to \left({A}{H}{B}={Z}\to {B}={Z}\right)\right)\right)\right)\right)$
50 49 rexlimiv ${⊢}\exists {a}\in {X}\phantom{\rule{.4em}{0ex}}{a}{H}{A}={U}\to \left({A}\in {X}\to \left({R}\in \mathrm{RingOps}\to \left({B}\in {X}\to \left({A}{H}{B}={Z}\to {B}={Z}\right)\right)\right)\right)$
51 50 com13 ${⊢}{R}\in \mathrm{RingOps}\to \left({A}\in {X}\to \left(\exists {a}\in {X}\phantom{\rule{.4em}{0ex}}{a}{H}{A}={U}\to \left({B}\in {X}\to \left({A}{H}{B}={Z}\to {B}={Z}\right)\right)\right)\right)$
52 51 3imp ${⊢}\left({R}\in \mathrm{RingOps}\wedge {A}\in {X}\wedge \exists {a}\in {X}\phantom{\rule{.4em}{0ex}}{a}{H}{A}={U}\right)\to \left({B}\in {X}\to \left({A}{H}{B}={Z}\to {B}={Z}\right)\right)$