Step | Hyp | Ref
| Expression |
1 | | isdomn3.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
2 | | eqid 2738 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
3 | | isdomn3.z |
. . 3
⊢ 0 =
(0g‘𝑅) |
4 | 1, 2, 3 | isdomn 20186 |
. 2
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
5 | | eqid 2738 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
6 | 5, 3 | isnzr 20151 |
. . . . 5
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ 0
)) |
7 | 6 | anbi1i 627 |
. . . 4
⊢ ((𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ 0 )
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
8 | | anass 472 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ 0 )
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝑅 ∈ Ring ∧
((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
9 | 7, 8 | bitri 278 |
. . 3
⊢ ((𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝑅 ∈ Ring ∧
((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
10 | 1, 5 | ringidcl 19440 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
11 | | eldifsn 4675 |
. . . . . . . 8
⊢
((1r‘𝑅) ∈ (𝐵 ∖ { 0 }) ↔
((1r‘𝑅)
∈ 𝐵 ∧
(1r‘𝑅)
≠ 0
)) |
12 | 11 | baibr 540 |
. . . . . . 7
⊢
((1r‘𝑅) ∈ 𝐵 → ((1r‘𝑅) ≠ 0 ↔
(1r‘𝑅)
∈ (𝐵 ∖ { 0
}))) |
13 | 10, 12 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
((1r‘𝑅)
≠ 0
↔ (1r‘𝑅) ∈ (𝐵 ∖ { 0 }))) |
14 | 1, 2 | ringcl 19433 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐵) |
15 | 14 | 3expb 1121 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐵) |
16 | 15 | biantrurd 536 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(.r‘𝑅)𝑦) ≠ 0 ↔ ((𝑥(.r‘𝑅)𝑦) ∈ 𝐵 ∧ (𝑥(.r‘𝑅)𝑦) ≠ 0 ))) |
17 | | eldifsn 4675 |
. . . . . . . . . 10
⊢ ((𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑥(.r‘𝑅)𝑦) ∈ 𝐵 ∧ (𝑥(.r‘𝑅)𝑦) ≠ 0 )) |
18 | 16, 17 | bitr4di 292 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(.r‘𝑅)𝑦) ≠ 0 ↔ (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
19 | 18 | imbi2d 344 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 ) ↔ ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
20 | 19 | 2ralbidva 3110 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 ) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
21 | | con34b 319 |
. . . . . . . . 9
⊢ (((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ (¬ (𝑥 = 0 ∨ 𝑦 = 0 ) → ¬ (𝑥(.r‘𝑅)𝑦) = 0 )) |
22 | | neanior 3026 |
. . . . . . . . . 10
⊢ ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ↔ ¬ (𝑥 = 0 ∨ 𝑦 = 0 )) |
23 | | df-ne 2935 |
. . . . . . . . . 10
⊢ ((𝑥(.r‘𝑅)𝑦) ≠ 0 ↔ ¬ (𝑥(.r‘𝑅)𝑦) = 0 ) |
24 | 22, 23 | imbi12i 354 |
. . . . . . . . 9
⊢ (((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 ) ↔ (¬ (𝑥 = 0 ∨ 𝑦 = 0 ) → ¬ (𝑥(.r‘𝑅)𝑦) = 0 )) |
25 | 21, 24 | bitr4i 281 |
. . . . . . . 8
⊢ (((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 )) |
26 | 25 | 2ralbii 3081 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 )) |
27 | | impexp 454 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
28 | | an4 656 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ))) |
29 | | eldifsn 4675 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) |
30 | | eldifsn 4675 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) |
31 | 29, 30 | anbi12i 630 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ))) |
32 | 28, 31 | bitr4i 281 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) ↔ (𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) |
33 | 32 | imbi1i 353 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
34 | 27, 33 | bitr3i 280 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) ↔ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
35 | 34 | 2albii 1827 |
. . . . . . . 8
⊢
(∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) ↔ ∀𝑥∀𝑦((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
36 | | r2al 3113 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
37 | | r2al 3113 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(𝐵 ∖ { 0
})∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ∀𝑥∀𝑦((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
38 | 35, 36, 37 | 3bitr4ri 307 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝐵 ∖ { 0
})∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
39 | 20, 26, 38 | 3bitr4g 317 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ ∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
40 | 13, 39 | anbi12d 634 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
41 | | isdomn3.u |
. . . . . . 7
⊢ 𝑈 = (mulGrp‘𝑅) |
42 | 41 | ringmgp 19422 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑈 ∈ Mnd) |
43 | 41, 1 | mgpbas 19364 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑈) |
44 | 41, 5 | ringidval 19372 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (0g‘𝑈) |
45 | 41, 2 | mgpplusg 19362 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (+g‘𝑈) |
46 | 43, 44, 45 | issubm 18084 |
. . . . . . . 8
⊢ (𝑈 ∈ Mnd → ((𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈) ↔
((𝐵 ∖ { 0 }) ⊆
𝐵 ∧
(1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
47 | | 3anass 1096 |
. . . . . . . 8
⊢ (((𝐵 ∖ { 0 }) ⊆ 𝐵 ∧
(1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝐵 ∖ { 0 }) ⊆ 𝐵 ∧
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
48 | 46, 47 | bitrdi 290 |
. . . . . . 7
⊢ (𝑈 ∈ Mnd → ((𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈) ↔
((𝐵 ∖ { 0 }) ⊆
𝐵 ∧
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))))) |
49 | | difss 4022 |
. . . . . . . 8
⊢ (𝐵 ∖ { 0 }) ⊆ 𝐵 |
50 | 49 | biantrur 534 |
. . . . . . 7
⊢
(((1r‘𝑅) ∈ (𝐵 ∖ { 0 }) ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝐵 ∖ { 0 }) ⊆ 𝐵 ∧
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
51 | 48, 50 | bitr4di 292 |
. . . . . 6
⊢ (𝑈 ∈ Mnd → ((𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈) ↔
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
52 | 42, 51 | syl 17 |
. . . . 5
⊢ (𝑅 ∈ Ring → ((𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈) ↔
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
53 | 40, 52 | bitr4d 285 |
. . . 4
⊢ (𝑅 ∈ Ring →
(((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |
54 | 53 | pm5.32i 578 |
. . 3
⊢ ((𝑅 ∈ Ring ∧
((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |
55 | 9, 54 | bitri 278 |
. 2
⊢ ((𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |
56 | 4, 55 | bitri 278 |
1
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |