Step |
Hyp |
Ref |
Expression |
1 |
|
isdomn3.b |
⊢ 𝐵 = ( Base ‘ 𝑅 ) |
2 |
|
isdomn3.z |
⊢ 0 = ( 0g ‘ 𝑅 ) |
3 |
|
isdomn3.u |
⊢ 𝑈 = ( mulGrp ‘ 𝑅 ) |
4 |
|
eqid |
⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 ) |
5 |
1 4 2
|
isdomn |
⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) |
6 |
|
eqid |
⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 ) |
7 |
6 2
|
isnzr |
⊢ ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ 0 ) ) |
8 |
7
|
anbi1i |
⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ↔ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ 0 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) |
9 |
|
anass |
⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ≠ 0 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ↔ ( 𝑅 ∈ Ring ∧ ( ( 1r ‘ 𝑅 ) ≠ 0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) ) |
10 |
8 9
|
bitri |
⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ↔ ( 𝑅 ∈ Ring ∧ ( ( 1r ‘ 𝑅 ) ≠ 0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) ) |
11 |
1 6
|
ringidcl |
⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 ) |
12 |
|
eldifsn |
⊢ ( ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( 1r ‘ 𝑅 ) ≠ 0 ) ) |
13 |
12
|
baibr |
⊢ ( ( 1r ‘ 𝑅 ) ∈ 𝐵 → ( ( 1r ‘ 𝑅 ) ≠ 0 ↔ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) |
14 |
11 13
|
syl |
⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ≠ 0 ↔ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) |
15 |
1 4
|
ringcl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 ) |
16 |
15
|
3expb |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 ) |
17 |
16
|
biantrurd |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ) ) ) |
18 |
|
eldifsn |
⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐵 ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ) ) |
19 |
17 18
|
bitr4di |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) |
20 |
19
|
imbi2d |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ) ↔ ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
21 |
20
|
2ralbidva |
⊢ ( 𝑅 ∈ Ring → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
22 |
|
con34b |
⊢ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ↔ ( ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) → ¬ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ) ) |
23 |
|
neanior |
⊢ ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ↔ ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) |
24 |
|
df-ne |
⊢ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ↔ ¬ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ) |
25 |
23 24
|
imbi12i |
⊢ ( ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ) ↔ ( ¬ ( 𝑥 = 0 ∨ 𝑦 = 0 ) → ¬ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ) ) |
26 |
22 25
|
bitr4i |
⊢ ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ↔ ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ) ) |
27 |
26
|
2ralbii |
⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 0 ) ) |
28 |
|
impexp |
⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
29 |
|
an4 |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) ) |
30 |
|
eldifsn |
⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) |
31 |
|
eldifsn |
⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) |
32 |
30 31
|
anbi12i |
⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) ) |
33 |
29 32
|
bitr4i |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ) ↔ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) |
34 |
33
|
imbi1i |
⊢ ( ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ↔ ( ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) |
35 |
28 34
|
bitr3i |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ↔ ( ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) |
36 |
35
|
2albii |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) |
37 |
|
r2al |
⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
38 |
|
r2al |
⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) |
39 |
36 37 38
|
3bitr4ri |
⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) |
40 |
21 27 39
|
3bitr4g |
⊢ ( 𝑅 ∈ Ring → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) |
41 |
14 40
|
anbi12d |
⊢ ( 𝑅 ∈ Ring → ( ( ( 1r ‘ 𝑅 ) ≠ 0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ↔ ( ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
42 |
3
|
ringmgp |
⊢ ( 𝑅 ∈ Ring → 𝑈 ∈ Mnd ) |
43 |
3 1
|
mgpbas |
⊢ 𝐵 = ( Base ‘ 𝑈 ) |
44 |
3 6
|
ringidval |
⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑈 ) |
45 |
3 4
|
mgpplusg |
⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑈 ) |
46 |
43 44 45
|
issubm |
⊢ ( 𝑈 ∈ Mnd → ( ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑈 ) ↔ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
47 |
|
3anass |
⊢ ( ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ↔ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 ∧ ( ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
48 |
46 47
|
bitrdi |
⊢ ( 𝑈 ∈ Mnd → ( ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑈 ) ↔ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 ∧ ( ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) ) |
49 |
|
difss |
⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 |
50 |
49
|
biantrur |
⊢ ( ( ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ↔ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 ∧ ( ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
51 |
48 50
|
bitr4di |
⊢ ( 𝑈 ∈ Mnd → ( ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑈 ) ↔ ( ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
52 |
42 51
|
syl |
⊢ ( 𝑅 ∈ Ring → ( ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑈 ) ↔ ( ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ { 0 } ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ) ) ) |
53 |
41 52
|
bitr4d |
⊢ ( 𝑅 ∈ Ring → ( ( ( 1r ‘ 𝑅 ) ≠ 0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ↔ ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑈 ) ) ) |
54 |
53
|
pm5.32i |
⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 1r ‘ 𝑅 ) ≠ 0 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ) ↔ ( 𝑅 ∈ Ring ∧ ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑈 ) ) ) |
55 |
10 54
|
bitri |
⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) ↔ ( 𝑅 ∈ Ring ∧ ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑈 ) ) ) |
56 |
5 55
|
bitri |
⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ Ring ∧ ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑈 ) ) ) |