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 = ( 1st ` R )
zerdivempx.2 
|- H = ( 2nd ` R )
zerdivempx.3 
|- Z = ( GId ` G )
zerdivempx.4 
|- X = ran G
zerdivempx.5 
|- U = ( GId ` H )
Assertion zerdivemp1x 
|- ( ( R e. RingOps /\ A e. X /\ E. a e. X ( a H A ) = U ) -> ( B e. X -> ( ( A H B ) = Z -> B = Z ) ) )

Proof

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