Metamath Proof Explorer

Theorem isdomn3

Description: Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015)

Ref Expression
Hypotheses isdomn3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdomn3.z ⊢ 0 = ( 0g ‘ 𝑅 )
isdomn3.u ⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
Assertion isdomn3 ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ Ring ∧ ( 𝐵 ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑈 ) ) )

Proof

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 ‘ 𝑈 ) ) )