Step | Hyp | Ref
| Expression |
1 | | isdomn3.b |
. . 3
⊢ 𝐵 = (Base‘𝑅) |
2 | | eqid 2622 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
3 | | isdomn3.z |
. . 3
⊢ 0 =
(0g‘𝑅) |
4 | 1, 2, 3 | isdomn 19294 |
. 2
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
5 | | eqid 2622 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
6 | 5, 3 | isnzr 19259 |
. . . . 5
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ 0
)) |
7 | 6 | anbi1i 731 |
. . . 4
⊢ ((𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ 0 )
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
8 | | anass 681 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ 0 )
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝑅 ∈ Ring ∧
((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
9 | 7, 8 | bitri 264 |
. . 3
⊢ ((𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝑅 ∈ Ring ∧
((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
10 | 1, 5 | ringidcl 18568 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
11 | | eldifsn 4317 |
. . . . . . . 8
⊢
((1r‘𝑅) ∈ (𝐵 ∖ { 0 }) ↔
((1r‘𝑅)
∈ 𝐵 ∧
(1r‘𝑅)
≠ 0
)) |
12 | 11 | baibr 945 |
. . . . . . 7
⊢
((1r‘𝑅) ∈ 𝐵 → ((1r‘𝑅) ≠ 0 ↔
(1r‘𝑅)
∈ (𝐵 ∖ { 0
}))) |
13 | 10, 12 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
((1r‘𝑅)
≠ 0
↔ (1r‘𝑅) ∈ (𝐵 ∖ { 0 }))) |
14 | 1, 2 | ringcl 18561 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐵) |
15 | 14 | 3expb 1266 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐵) |
16 | 15 | biantrurd 529 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(.r‘𝑅)𝑦) ≠ 0 ↔ ((𝑥(.r‘𝑅)𝑦) ∈ 𝐵 ∧ (𝑥(.r‘𝑅)𝑦) ≠ 0 ))) |
17 | | eldifsn 4317 |
. . . . . . . . . 10
⊢ ((𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑥(.r‘𝑅)𝑦) ∈ 𝐵 ∧ (𝑥(.r‘𝑅)𝑦) ≠ 0 )) |
18 | 16, 17 | syl6bbr 278 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(.r‘𝑅)𝑦) ≠ 0 ↔ (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
19 | 18 | imbi2d 330 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 ) ↔ ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
20 | 19 | 2ralbidva 2988 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 ) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
21 | | con34b 306 |
. . . . . . . . 9
⊢ (((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ (¬ (𝑥 = 0 ∨ 𝑦 = 0 ) → ¬ (𝑥(.r‘𝑅)𝑦) = 0 )) |
22 | | neanior 2886 |
. . . . . . . . . 10
⊢ ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ↔ ¬ (𝑥 = 0 ∨ 𝑦 = 0 )) |
23 | | df-ne 2795 |
. . . . . . . . . 10
⊢ ((𝑥(.r‘𝑅)𝑦) ≠ 0 ↔ ¬ (𝑥(.r‘𝑅)𝑦) = 0 ) |
24 | 22, 23 | imbi12i 340 |
. . . . . . . . 9
⊢ (((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 ) ↔ (¬ (𝑥 = 0 ∨ 𝑦 = 0 ) → ¬ (𝑥(.r‘𝑅)𝑦) = 0 )) |
25 | 21, 24 | bitr4i 267 |
. . . . . . . 8
⊢ (((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 )) |
26 | 25 | 2ralbii 2981 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 )) |
27 | | impexp 462 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
28 | | an4 865 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ))) |
29 | | eldifsn 4317 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) |
30 | | eldifsn 4317 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) |
31 | 29, 30 | anbi12i 733 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ))) |
32 | 28, 31 | bitr4i 267 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) ↔ (𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) |
33 | 32 | imbi1i 339 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
34 | 27, 33 | bitr3i 266 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) ↔ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
35 | 34 | 2albii 1748 |
. . . . . . . 8
⊢
(∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) ↔ ∀𝑥∀𝑦((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
36 | | r2al 2939 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
37 | | r2al 2939 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(𝐵 ∖ { 0
})∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ∀𝑥∀𝑦((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
38 | 35, 36, 37 | 3bitr4ri 293 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝐵 ∖ { 0
})∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
39 | 20, 26, 38 | 3bitr4g 303 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ ∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
40 | 13, 39 | anbi12d 747 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
41 | | isdomn3.u |
. . . . . . 7
⊢ 𝑈 = (mulGrp‘𝑅) |
42 | 41 | ringmgp 18553 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑈 ∈ Mnd) |
43 | 41, 1 | mgpbas 18495 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑈) |
44 | 41, 5 | ringidval 18503 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (0g‘𝑈) |
45 | 41, 2 | mgpplusg 18493 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (+g‘𝑈) |
46 | 43, 44, 45 | issubm 17347 |
. . . . . . . 8
⊢ (𝑈 ∈ Mnd → ((𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈) ↔
((𝐵 ∖ { 0 }) ⊆
𝐵 ∧
(1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
47 | | 3anass 1042 |
. . . . . . . 8
⊢ (((𝐵 ∖ { 0 }) ⊆ 𝐵 ∧
(1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝐵 ∖ { 0 }) ⊆ 𝐵 ∧
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
48 | 46, 47 | syl6bb 276 |
. . . . . . 7
⊢ (𝑈 ∈ Mnd → ((𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈) ↔
((𝐵 ∖ { 0 }) ⊆
𝐵 ∧
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))))) |
49 | | difss 3737 |
. . . . . . . 8
⊢ (𝐵 ∖ { 0 }) ⊆ 𝐵 |
50 | 49 | biantrur 527 |
. . . . . . 7
⊢
(((1r‘𝑅) ∈ (𝐵 ∖ { 0 }) ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝐵 ∖ { 0 }) ⊆ 𝐵 ∧
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
51 | 48, 50 | syl6bbr 278 |
. . . . . 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 271 |
. . . 4
⊢ (𝑅 ∈ Ring →
(((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |
54 | 53 | pm5.32i 669 |
. . 3
⊢ ((𝑅 ∈ Ring ∧
((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |
55 | 9, 54 | bitri 264 |
. 2
⊢ ((𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |
56 | 4, 55 | bitri 264 |
1
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |