Metamath Proof Explorer


Theorem ringinvnzdiv

Description: In a unital ring, a left invertible element is not a zero divisor. (Contributed by FL, 18-Apr-2010) (Revised by Jeff Madsen, 18-Apr-2010) (Revised by AV, 24-Aug-2021)

Ref Expression
Hypotheses ringinvnzdiv.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
ringinvnzdiv.t โŠข ยท = ( .r โ€˜ ๐‘… )
ringinvnzdiv.u โŠข 1 = ( 1r โ€˜ ๐‘… )
ringinvnzdiv.z โŠข 0 = ( 0g โ€˜ ๐‘… )
ringinvnzdiv.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
ringinvnzdiv.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
ringinvnzdiv.a โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘Ž โˆˆ ๐ต ( ๐‘Ž ยท ๐‘‹ ) = 1 )
ringinvnzdiv.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
Assertion ringinvnzdiv ( ๐œ‘ โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) = 0 โ†” ๐‘Œ = 0 ) )

Proof

Step Hyp Ref Expression
1 ringinvnzdiv.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
2 ringinvnzdiv.t โŠข ยท = ( .r โ€˜ ๐‘… )
3 ringinvnzdiv.u โŠข 1 = ( 1r โ€˜ ๐‘… )
4 ringinvnzdiv.z โŠข 0 = ( 0g โ€˜ ๐‘… )
5 ringinvnzdiv.r โŠข ( ๐œ‘ โ†’ ๐‘… โˆˆ Ring )
6 ringinvnzdiv.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต )
7 ringinvnzdiv.a โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘Ž โˆˆ ๐ต ( ๐‘Ž ยท ๐‘‹ ) = 1 )
8 ringinvnzdiv.y โŠข ( ๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต )
9 1 2 3 ringlidm โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘Œ โˆˆ ๐ต ) โ†’ ( 1 ยท ๐‘Œ ) = ๐‘Œ )
10 5 8 9 syl2anc โŠข ( ๐œ‘ โ†’ ( 1 ยท ๐‘Œ ) = ๐‘Œ )
11 10 eqcomd โŠข ( ๐œ‘ โ†’ ๐‘Œ = ( 1 ยท ๐‘Œ ) )
12 11 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โˆง ( ๐‘Ž ยท ๐‘‹ ) = 1 ) โˆง ( ๐‘‹ ยท ๐‘Œ ) = 0 ) โ†’ ๐‘Œ = ( 1 ยท ๐‘Œ ) )
13 oveq1 โŠข ( 1 = ( ๐‘Ž ยท ๐‘‹ ) โ†’ ( 1 ยท ๐‘Œ ) = ( ( ๐‘Ž ยท ๐‘‹ ) ยท ๐‘Œ ) )
14 13 eqcoms โŠข ( ( ๐‘Ž ยท ๐‘‹ ) = 1 โ†’ ( 1 ยท ๐‘Œ ) = ( ( ๐‘Ž ยท ๐‘‹ ) ยท ๐‘Œ ) )
15 14 adantl โŠข ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โˆง ( ๐‘Ž ยท ๐‘‹ ) = 1 ) โ†’ ( 1 ยท ๐‘Œ ) = ( ( ๐‘Ž ยท ๐‘‹ ) ยท ๐‘Œ ) )
16 5 adantr โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โ†’ ๐‘… โˆˆ Ring )
17 simpr โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โ†’ ๐‘Ž โˆˆ ๐ต )
18 6 adantr โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โ†’ ๐‘‹ โˆˆ ๐ต )
19 8 adantr โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โ†’ ๐‘Œ โˆˆ ๐ต )
20 17 18 19 3jca โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โ†’ ( ๐‘Ž โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) )
21 16 20 jca โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โ†’ ( ๐‘… โˆˆ Ring โˆง ( ๐‘Ž โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) )
22 21 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โˆง ( ๐‘Ž ยท ๐‘‹ ) = 1 ) โ†’ ( ๐‘… โˆˆ Ring โˆง ( ๐‘Ž โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) )
23 1 2 ringass โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘Ž โˆˆ ๐ต โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘Ž ยท ๐‘‹ ) ยท ๐‘Œ ) = ( ๐‘Ž ยท ( ๐‘‹ ยท ๐‘Œ ) ) )
24 22 23 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โˆง ( ๐‘Ž ยท ๐‘‹ ) = 1 ) โ†’ ( ( ๐‘Ž ยท ๐‘‹ ) ยท ๐‘Œ ) = ( ๐‘Ž ยท ( ๐‘‹ ยท ๐‘Œ ) ) )
25 15 24 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โˆง ( ๐‘Ž ยท ๐‘‹ ) = 1 ) โ†’ ( 1 ยท ๐‘Œ ) = ( ๐‘Ž ยท ( ๐‘‹ ยท ๐‘Œ ) ) )
26 25 adantr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โˆง ( ๐‘Ž ยท ๐‘‹ ) = 1 ) โˆง ( ๐‘‹ ยท ๐‘Œ ) = 0 ) โ†’ ( 1 ยท ๐‘Œ ) = ( ๐‘Ž ยท ( ๐‘‹ ยท ๐‘Œ ) ) )
27 oveq2 โŠข ( ( ๐‘‹ ยท ๐‘Œ ) = 0 โ†’ ( ๐‘Ž ยท ( ๐‘‹ ยท ๐‘Œ ) ) = ( ๐‘Ž ยท 0 ) )
28 1 2 4 ringrz โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘Ž โˆˆ ๐ต ) โ†’ ( ๐‘Ž ยท 0 ) = 0 )
29 5 28 sylan โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โ†’ ( ๐‘Ž ยท 0 ) = 0 )
30 29 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โˆง ( ๐‘Ž ยท ๐‘‹ ) = 1 ) โ†’ ( ๐‘Ž ยท 0 ) = 0 )
31 27 30 sylan9eqr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โˆง ( ๐‘Ž ยท ๐‘‹ ) = 1 ) โˆง ( ๐‘‹ ยท ๐‘Œ ) = 0 ) โ†’ ( ๐‘Ž ยท ( ๐‘‹ ยท ๐‘Œ ) ) = 0 )
32 12 26 31 3eqtrd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โˆง ( ๐‘Ž ยท ๐‘‹ ) = 1 ) โˆง ( ๐‘‹ ยท ๐‘Œ ) = 0 ) โ†’ ๐‘Œ = 0 )
33 32 exp31 โŠข ( ( ๐œ‘ โˆง ๐‘Ž โˆˆ ๐ต ) โ†’ ( ( ๐‘Ž ยท ๐‘‹ ) = 1 โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) = 0 โ†’ ๐‘Œ = 0 ) ) )
34 33 rexlimdva โŠข ( ๐œ‘ โ†’ ( โˆƒ ๐‘Ž โˆˆ ๐ต ( ๐‘Ž ยท ๐‘‹ ) = 1 โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) = 0 โ†’ ๐‘Œ = 0 ) ) )
35 7 34 mpd โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) = 0 โ†’ ๐‘Œ = 0 ) )
36 oveq2 โŠข ( ๐‘Œ = 0 โ†’ ( ๐‘‹ ยท ๐‘Œ ) = ( ๐‘‹ ยท 0 ) )
37 1 2 4 ringrz โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐ต ) โ†’ ( ๐‘‹ ยท 0 ) = 0 )
38 5 6 37 syl2anc โŠข ( ๐œ‘ โ†’ ( ๐‘‹ ยท 0 ) = 0 )
39 36 38 sylan9eqr โŠข ( ( ๐œ‘ โˆง ๐‘Œ = 0 ) โ†’ ( ๐‘‹ ยท ๐‘Œ ) = 0 )
40 39 ex โŠข ( ๐œ‘ โ†’ ( ๐‘Œ = 0 โ†’ ( ๐‘‹ ยท ๐‘Œ ) = 0 ) )
41 35 40 impbid โŠข ( ๐œ‘ โ†’ ( ( ๐‘‹ ยท ๐‘Œ ) = 0 โ†” ๐‘Œ = 0 ) )