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

Metamath Proof Explorer

Theorem drngidl

Description: A nonzero ring is a division ring if and only if its only left ideals are the zero ideal and the unit ideal. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025)

Ref Expression
Hypotheses drngidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
drngidl.z ⊢ 0 = ( 0g ‘ 𝑅 )
drngidl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
Assertion drngidl ( 𝑅 ∈ NzRing → ( 𝑅 ∈ DivRing ↔ 𝑈 = { { 0 } , 𝐵 } ) )

Proof

Step Hyp Ref Expression
1 drngidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 drngidl.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 drngidl.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
4 1 2 3 drngnidl ⊢ ( 𝑅 ∈ DivRing → 𝑈 = { { 0 } , 𝐵 } )
5 4 adantl ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑅 ∈ DivRing ) → 𝑈 = { { 0 } , 𝐵 } )
6 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
7 6 2 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
8 7 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → ( 1r ‘ 𝑅 ) ≠ 0 )
9 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
11 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
12 11 adantr ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → 𝑅 ∈ Ring )
13 12 adantr ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑅 ∈ Ring )
14 13 ad4antr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑅 ∈ Ring )
15 simp-4r ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑦 ∈ 𝐵 )
16 simplr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑧 ∈ 𝐵 )
17 simpr ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ∈ ( 𝐵 ∖ { 0 } ) )
18 17 eldifad ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ∈ 𝐵 )
19 18 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑥 ∈ 𝐵 )
20 19 ad2antrr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑥 ∈ 𝐵 )
21 simpr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) )
22 21 eqcomd ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) = ( 1r ‘ 𝑅 ) )
23 simpr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
24 23 eqcomd ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
25 24 ad2antrr ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) )
26 1 2 6 9 10 14 15 16 20 22 25 ringinveu ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → 𝑥 = 𝑧 )
27 26 oveq1d ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) )
28 27 22 eqtrd ⊢ ( ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 1r ‘ 𝑅 ) )
29 13 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑅 ∈ Ring )
30 simplr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑦 ∈ 𝐵 )
31 1 6 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
32 13 31 syl ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
33 32 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
34 30 snssd ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → { 𝑦 } ⊆ 𝐵 )
35 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
36 35 1 3 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑦 } ⊆ 𝐵 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ∈ 𝑈 )
37 29 34 36 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ∈ 𝑈 )
38 simp-4r ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑈 = { { 0 } , 𝐵 } )
39 37 38 eleqtrd ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ∈ { { 0 } , 𝐵 } )
40 elpri ⊢ ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ∈ { { 0 } , 𝐵 } → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) = { 0 } ∨ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) = 𝐵 ) )
41 39 40 syl ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) = { 0 } ∨ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) = 𝐵 ) )
42 simplr ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑦 = 0 ) → ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
43 simpr ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑦 = 0 ) → 𝑦 = 0 )
44 43 oveq1d ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑦 = 0 ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 0 ( .r ‘ 𝑅 ) 𝑥 ) )
45 1 9 2 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 0 ( .r ‘ 𝑅 ) 𝑥 ) = 0 )
46 13 18 45 syl2anc ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 0 ( .r ‘ 𝑅 ) 𝑥 ) = 0 )
47 46 ad3antrrr ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑦 = 0 ) → ( 0 ( .r ‘ 𝑅 ) 𝑥 ) = 0 )
48 42 44 47 3eqtrd ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑦 = 0 ) → ( 1r ‘ 𝑅 ) = 0 )
49 8 ad4antr ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑦 = 0 ) → ( 1r ‘ 𝑅 ) ≠ 0 )
50 49 neneqd ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ∧ 𝑦 = 0 ) → ¬ ( 1r ‘ 𝑅 ) = 0 )
51 48 50 pm2.65da ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ¬ 𝑦 = 0 )
52 51 neqned ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → 𝑦 ≠ 0 )
53 1 2 35 pidlnz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ≠ { 0 } )
54 29 30 52 53 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ≠ { 0 } )
55 54 neneqd ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ¬ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) = { 0 } )
56 41 55 orcnd ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) = 𝐵 )
57 33 56 eleqtrrd ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) )
58 1 9 35 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ↔ ∃ 𝑧 ∈ 𝐵 ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) )
59 58 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑦 } ) ) → ∃ 𝑧 ∈ 𝐵 ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) )
60 29 30 57 59 syl21anc ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ∃ 𝑧 ∈ 𝐵 ( 1r ‘ 𝑅 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) )
61 28 60 r19.29a ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 1r ‘ 𝑅 ) )
62 61 24 jca ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
63 62 anasss ⊢ ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
64 18 snssd ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → { 𝑥 } ⊆ 𝐵 )
65 35 1 3 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑥 } ⊆ 𝐵 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ 𝑈 )
66 13 64 65 syl2anc ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ 𝑈 )
67 simplr ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑈 = { { 0 } , 𝐵 } )
68 66 67 eleqtrd ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ { { 0 } , 𝐵 } )
69 elpri ⊢ ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ∈ { { 0 } , 𝐵 } → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) = { 0 } ∨ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) = 𝐵 ) )
70 68 69 syl ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) = { 0 } ∨ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) = 𝐵 ) )
71 eldifsni ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ≠ 0 )
72 71 adantl ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ≠ 0 )
73 1 2 35 pidlnz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ≠ { 0 } )
74 13 18 72 73 syl3anc ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ≠ { 0 } )
75 74 neneqd ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ¬ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) = { 0 } )
76 70 75 orcnd ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) = 𝐵 )
77 32 76 eleqtrrd ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) )
78 1 9 35 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ↔ ∃ 𝑦 ∈ 𝐵 ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) )
79 78 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1r ‘ 𝑅 ) ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑥 } ) ) → ∃ 𝑦 ∈ 𝐵 ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
80 13 18 77 79 syl21anc ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ∃ 𝑦 ∈ 𝐵 ( 1r ‘ 𝑅 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
81 63 80 reximddv ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
82 81 ralrimiva ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) )
83 1 2 6 9 10 12 isdrng4 ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → ( 𝑅 ∈ DivRing ↔ ( ( 1r ‘ 𝑅 ) ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( 1r ‘ 𝑅 ) ) ) ) )
84 8 82 83 mpbir2and ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑈 = { { 0 } , 𝐵 } ) → 𝑅 ∈ DivRing )
85 5 84 impbida ⊢ ( 𝑅 ∈ NzRing → ( 𝑅 ∈ DivRing ↔ 𝑈 = { { 0 } , 𝐵 } ) )