This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zerdivemp1x

Description: In a unital 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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
zerdivempx.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
zerdivempx.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
zerdivempx.4 ⊢ 𝑋 = ran 𝐺
zerdivempx.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion zerdivemp1x ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ( 𝑎 𝐻 𝐴 ) = 𝑈 ) → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → 𝐵 = 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 zerdivempx.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 zerdivempx.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 zerdivempx.3 ⊢ 𝑍 = ( GId ‘ 𝐺 )
4 zerdivempx.4 ⊢ 𝑋 = ran 𝐺
5 zerdivempx.5 ⊢ 𝑈 = ( GId ‘ 𝐻 )
6 oveq2 ⊢ ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) )
7 simpl1 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) ) → 𝑅 ∈ RingOps )
8 simpr1 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) ) → 𝑎 ∈ 𝑋 )
9 simpr3 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 )
10 simpl3 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
11 1 2 4 rngoass ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝑎 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) )
12 7 8 9 10 11 syl13anc ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) )
13 eqtr ⊢ ( ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) ∧ ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) ) → ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) )
14 13 ex ⊢ ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) → ( ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) → ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) ) )
15 eqtr ⊢ ( ( ( 𝑈 𝐻 𝐵 ) = ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) ∧ ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) ) → ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) )
16 3 4 1 2 rngorz ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑎 ∈ 𝑋 ) → ( 𝑎 𝐻 𝑍 ) = 𝑍 )
17 16 3adant3 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑎 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑎 𝐻 𝑍 ) = 𝑍 )
18 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
19 4 18 eqtri ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
20 2 19 5 rngolidm ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐵 ∈ 𝑋 ) → ( 𝑈 𝐻 𝐵 ) = 𝐵 )
21 20 3adant2 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑎 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑈 𝐻 𝐵 ) = 𝐵 )
22 simp1 ⊢ ( ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) ∧ ( 𝑈 𝐻 𝐵 ) = 𝐵 ∧ ( 𝑎 𝐻 𝑍 ) = 𝑍 ) → ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) )
23 simp2 ⊢ ( ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) ∧ ( 𝑈 𝐻 𝐵 ) = 𝐵 ∧ ( 𝑎 𝐻 𝑍 ) = 𝑍 ) → ( 𝑈 𝐻 𝐵 ) = 𝐵 )
24 simp3 ⊢ ( ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) ∧ ( 𝑈 𝐻 𝐵 ) = 𝐵 ∧ ( 𝑎 𝐻 𝑍 ) = 𝑍 ) → ( 𝑎 𝐻 𝑍 ) = 𝑍 )
25 22 23 24 3eqtr3d ⊢ ( ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) ∧ ( 𝑈 𝐻 𝐵 ) = 𝐵 ∧ ( 𝑎 𝐻 𝑍 ) = 𝑍 ) → 𝐵 = 𝑍 )
26 25 a1d ⊢ ( ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) ∧ ( 𝑈 𝐻 𝐵 ) = 𝐵 ∧ ( 𝑎 𝐻 𝑍 ) = 𝑍 ) → ( 𝐴 ∈ 𝑋 → 𝐵 = 𝑍 ) )
27 26 3exp ⊢ ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → ( ( 𝑈 𝐻 𝐵 ) = 𝐵 → ( ( 𝑎 𝐻 𝑍 ) = 𝑍 → ( 𝐴 ∈ 𝑋 → 𝐵 = 𝑍 ) ) ) )
28 27 com14 ⊢ ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐵 ) = 𝐵 → ( ( 𝑎 𝐻 𝑍 ) = 𝑍 → ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → 𝐵 = 𝑍 ) ) ) )
29 28 com13 ⊢ ( ( 𝑎 𝐻 𝑍 ) = 𝑍 → ( ( 𝑈 𝐻 𝐵 ) = 𝐵 → ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → 𝐵 = 𝑍 ) ) ) )
30 17 21 29 sylc ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑎 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → 𝐵 = 𝑍 ) ) )
31 30 3exp ⊢ ( 𝑅 ∈ RingOps → ( 𝑎 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → 𝐵 = 𝑍 ) ) ) ) )
32 31 com15 ⊢ ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → ( 𝑎 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) ) )
33 32 com24 ⊢ ( ( 𝑈 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝑎 ∈ 𝑋 → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) ) )
34 15 33 syl ⊢ ( ( ( 𝑈 𝐻 𝐵 ) = ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) ∧ ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) ) → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝑎 ∈ 𝑋 → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) ) )
35 34 ex ⊢ ( ( 𝑈 𝐻 𝐵 ) = ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) → ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝑎 ∈ 𝑋 → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) ) ) )
36 35 eqcoms ⊢ ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑈 𝐻 𝐵 ) → ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝑎 ∈ 𝑋 → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) ) ) )
37 36 com25 ⊢ ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑈 𝐻 𝐵 ) → ( 𝑎 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) ) ) )
38 oveq1 ⊢ ( ( 𝑎 𝐻 𝐴 ) = 𝑈 → ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑈 𝐻 𝐵 ) )
39 37 38 syl11 ⊢ ( 𝑎 ∈ 𝑋 → ( ( 𝑎 𝐻 𝐴 ) = 𝑈 → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) ) ) )
40 39 3imp ⊢ ( ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 ∈ 𝑋 → ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) )
41 40 com13 ⊢ ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 𝑍 ) → ( 𝐵 ∈ 𝑋 → ( ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) )
42 14 41 syl6 ⊢ ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) → ( ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) → ( 𝐵 ∈ 𝑋 → ( ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑅 ∈ RingOps → 𝐵 = 𝑍 ) ) ) ) )
43 42 com15 ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) → ( 𝐵 ∈ 𝑋 → ( ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) → 𝐵 = 𝑍 ) ) ) ) )
44 43 3imp1 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( ( 𝑎 𝐻 𝐴 ) 𝐻 𝐵 ) = ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) → 𝐵 = 𝑍 ) )
45 12 44 mpd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) ) → 𝐵 = 𝑍 )
46 45 3exp1 ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑎 𝐻 ( 𝐴 𝐻 𝐵 ) ) = ( 𝑎 𝐻 𝑍 ) → ( 𝐵 ∈ 𝑋 → ( ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) → 𝐵 = 𝑍 ) ) ) )
47 6 46 syl5com ⊢ ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → ( 𝑅 ∈ RingOps → ( 𝐵 ∈ 𝑋 → ( ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) → 𝐵 = 𝑍 ) ) ) )
48 47 com14 ⊢ ( ( 𝑎 ∈ 𝑋 ∧ ( 𝑎 𝐻 𝐴 ) = 𝑈 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑅 ∈ RingOps → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → 𝐵 = 𝑍 ) ) ) )
49 48 3exp ⊢ ( 𝑎 ∈ 𝑋 → ( ( 𝑎 𝐻 𝐴 ) = 𝑈 → ( 𝐴 ∈ 𝑋 → ( 𝑅 ∈ RingOps → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → 𝐵 = 𝑍 ) ) ) ) ) )
50 49 rexlimiv ⊢ ( ∃ 𝑎 ∈ 𝑋 ( 𝑎 𝐻 𝐴 ) = 𝑈 → ( 𝐴 ∈ 𝑋 → ( 𝑅 ∈ RingOps → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → 𝐵 = 𝑍 ) ) ) ) )
51 50 com13 ⊢ ( 𝑅 ∈ RingOps → ( 𝐴 ∈ 𝑋 → ( ∃ 𝑎 ∈ 𝑋 ( 𝑎 𝐻 𝐴 ) = 𝑈 → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → 𝐵 = 𝑍 ) ) ) ) )
52 51 3imp ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ ∃ 𝑎 ∈ 𝑋 ( 𝑎 𝐻 𝐴 ) = 𝑈 ) → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) = 𝑍 → 𝐵 = 𝑍 ) ) )