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 20565 |
. 2
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
5 | | eqid 2738 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
6 | 5, 3 | isnzr 20530 |
. . . . 5
⊢ (𝑅 ∈ NzRing ↔ (𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ 0
)) |
7 | 6 | anbi1i 624 |
. . . 4
⊢ ((𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ 0 )
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) |
8 | | anass 469 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧
(1r‘𝑅)
≠ 0 )
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝑅 ∈ Ring ∧
((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
9 | 7, 8 | bitri 274 |
. . 3
⊢ ((𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝑅 ∈ Ring ∧
((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))))) |
10 | 1, 5 | ringidcl 19807 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
11 | | eldifsn 4720 |
. . . . . . . 8
⊢
((1r‘𝑅) ∈ (𝐵 ∖ { 0 }) ↔
((1r‘𝑅)
∈ 𝐵 ∧
(1r‘𝑅)
≠ 0
)) |
12 | 11 | baibr 537 |
. . . . . . 7
⊢
((1r‘𝑅) ∈ 𝐵 → ((1r‘𝑅) ≠ 0 ↔
(1r‘𝑅)
∈ (𝐵 ∖ { 0
}))) |
13 | 10, 12 | syl 17 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
((1r‘𝑅)
≠ 0
↔ (1r‘𝑅) ∈ (𝐵 ∖ { 0 }))) |
14 | 1, 2 | ringcl 19800 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐵) |
15 | 14 | 3expb 1119 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝑅)𝑦) ∈ 𝐵) |
16 | 15 | biantrurd 533 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(.r‘𝑅)𝑦) ≠ 0 ↔ ((𝑥(.r‘𝑅)𝑦) ∈ 𝐵 ∧ (𝑥(.r‘𝑅)𝑦) ≠ 0 ))) |
17 | | eldifsn 4720 |
. . . . . . . . . 10
⊢ ((𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ((𝑥(.r‘𝑅)𝑦) ∈ 𝐵 ∧ (𝑥(.r‘𝑅)𝑦) ≠ 0 )) |
18 | 16, 17 | bitr4di 289 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥(.r‘𝑅)𝑦) ≠ 0 ↔ (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
19 | 18 | imbi2d 341 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 ) ↔ ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
20 | 19 | 2ralbidva 3128 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 ) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
21 | | con34b 316 |
. . . . . . . . 9
⊢ (((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ (¬ (𝑥 = 0 ∨ 𝑦 = 0 ) → ¬ (𝑥(.r‘𝑅)𝑦) = 0 )) |
22 | | neanior 3037 |
. . . . . . . . . 10
⊢ ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) ↔ ¬ (𝑥 = 0 ∨ 𝑦 = 0 )) |
23 | | df-ne 2944 |
. . . . . . . . . 10
⊢ ((𝑥(.r‘𝑅)𝑦) ≠ 0 ↔ ¬ (𝑥(.r‘𝑅)𝑦) = 0 ) |
24 | 22, 23 | imbi12i 351 |
. . . . . . . . 9
⊢ (((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 ) ↔ (¬ (𝑥 = 0 ∨ 𝑦 = 0 ) → ¬ (𝑥(.r‘𝑅)𝑦) = 0 )) |
25 | 21, 24 | bitr4i 277 |
. . . . . . . 8
⊢ (((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 )) |
26 | 25 | 2ralbii 3093 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ≠ 0 )) |
27 | | impexp 451 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
28 | | an4 653 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ))) |
29 | | eldifsn 4720 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐵 ∖ { 0 }) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 )) |
30 | | eldifsn 4720 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝐵 ∖ { 0 }) ↔ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 )) |
31 | 29, 30 | anbi12i 627 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ (𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ))) |
32 | 28, 31 | bitr4i 277 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) ↔ (𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 }))) |
33 | 32 | imbi1i 350 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝑥 ≠ 0 ∧ 𝑦 ≠ 0 )) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
34 | 27, 33 | bitr3i 276 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) ↔ ((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
35 | 34 | 2albii 1823 |
. . . . . . . 8
⊢
(∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) ↔ ∀𝑥∀𝑦((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
36 | | r2al 3118 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
37 | | r2al 3118 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(𝐵 ∖ { 0
})∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ∀𝑥∀𝑦((𝑥 ∈ (𝐵 ∖ { 0 }) ∧ 𝑦 ∈ (𝐵 ∖ { 0 })) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
38 | 35, 36, 37 | 3bitr4ri 304 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝐵 ∖ { 0
})∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ≠ 0 ∧ 𝑦 ≠ 0 ) → (𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
39 | 20, 26, 38 | 3bitr4g 314 |
. . . . . 6
⊢ (𝑅 ∈ Ring →
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )) ↔ ∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))) |
40 | 13, 39 | anbi12d 631 |
. . . . 5
⊢ (𝑅 ∈ Ring →
(((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
41 | | isdomn3.u |
. . . . . . 7
⊢ 𝑈 = (mulGrp‘𝑅) |
42 | 41 | ringmgp 19789 |
. . . . . 6
⊢ (𝑅 ∈ Ring → 𝑈 ∈ Mnd) |
43 | 41, 1 | mgpbas 19726 |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑈) |
44 | 41, 5 | ringidval 19739 |
. . . . . . . . 9
⊢
(1r‘𝑅) = (0g‘𝑈) |
45 | 41, 2 | mgpplusg 19724 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (+g‘𝑈) |
46 | 43, 44, 45 | issubm 18442 |
. . . . . . . 8
⊢ (𝑈 ∈ Mnd → ((𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈) ↔
((𝐵 ∖ { 0 }) ⊆
𝐵 ∧
(1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
47 | | 3anass 1094 |
. . . . . . . 8
⊢ (((𝐵 ∖ { 0 }) ⊆ 𝐵 ∧
(1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝐵 ∖ { 0 }) ⊆ 𝐵 ∧
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
48 | 46, 47 | bitrdi 287 |
. . . . . . 7
⊢ (𝑈 ∈ Mnd → ((𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈) ↔
((𝐵 ∖ { 0 }) ⊆
𝐵 ∧
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 }))))) |
49 | | difss 4066 |
. . . . . . . 8
⊢ (𝐵 ∖ { 0 }) ⊆ 𝐵 |
50 | 49 | biantrur 531 |
. . . . . . 7
⊢
(((1r‘𝑅) ∈ (𝐵 ∖ { 0 }) ∧ ∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })) ↔ ((𝐵 ∖ { 0 }) ⊆ 𝐵 ∧
((1r‘𝑅)
∈ (𝐵 ∖ { 0 }) ∧
∀𝑥 ∈ (𝐵 ∖ { 0 })∀𝑦 ∈ (𝐵 ∖ { 0 })(𝑥(.r‘𝑅)𝑦) ∈ (𝐵 ∖ { 0 })))) |
51 | 48, 50 | bitr4di 289 |
. . . . . 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 281 |
. . . 4
⊢ (𝑅 ∈ Ring →
(((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |
54 | 53 | pm5.32i 575 |
. . 3
⊢ ((𝑅 ∈ Ring ∧
((1r‘𝑅)
≠ 0
∧ ∀𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 )))) ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |
55 | 9, 54 | bitri 274 |
. 2
⊢ ((𝑅 ∈ NzRing ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥(.r‘𝑅)𝑦) = 0 → (𝑥 = 0 ∨ 𝑦 = 0 ))) ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |
56 | 4, 55 | bitri 274 |
1
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ Ring ∧ (𝐵 ∖ { 0 }) ∈
(SubMnd‘𝑈))) |