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