Proof of Theorem isdomn4
Step | Hyp | Ref
| Expression |
1 | | domnnzr 20363 |
. . 3
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
2 | | isdomn4.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
3 | | isdomn4.x |
. . . . . . . 8
⊢ · =
(.r‘𝑅) |
4 | | eqid 2739 |
. . . . . . . 8
⊢
(-g‘𝑅) = (-g‘𝑅) |
5 | | domnring 20364 |
. . . . . . . . 9
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Ring) |
6 | 5 | adantr 484 |
. . . . . . . 8
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑅 ∈ Ring) |
7 | | eldifi 4057 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝐵 ∖ { 0 }) → 𝑎 ∈ 𝐵) |
8 | 7 | 3ad2ant1 1135 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
9 | 8 | adantl 485 |
. . . . . . . 8
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
10 | | simpr2 1197 |
. . . . . . . 8
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
11 | | simpr3 1198 |
. . . . . . . 8
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑐 ∈ 𝐵) |
12 | 2, 3, 4, 6, 9, 10,
11 | ringsubdi 19647 |
. . . . . . 7
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎 · (𝑏(-g‘𝑅)𝑐)) = ((𝑎 · 𝑏)(-g‘𝑅)(𝑎 · 𝑐))) |
13 | 12 | eqeq1d 2741 |
. . . . . 6
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎 · (𝑏(-g‘𝑅)𝑐)) = 0 ↔ ((𝑎 · 𝑏)(-g‘𝑅)(𝑎 · 𝑐)) = 0 )) |
14 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑏(-g‘𝑅)𝑐) ≠ 0 ) → 𝑅 ∈ Domn) |
15 | 9 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑏(-g‘𝑅)𝑐) ≠ 0 ) → 𝑎 ∈ 𝐵) |
16 | | eldifsni 4719 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝐵 ∖ { 0 }) → 𝑎 ≠ 0 ) |
17 | 16 | 3ad2ant1 1135 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → 𝑎 ≠ 0 ) |
18 | 17 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑏(-g‘𝑅)𝑐) ≠ 0 ) → 𝑎 ≠ 0 ) |
19 | 5 | ringgrpd 19601 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ Domn → 𝑅 ∈ Grp) |
20 | 2, 4 | grpsubcl 18473 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑏(-g‘𝑅)𝑐) ∈ 𝐵) |
21 | 19, 20 | syl3an1 1165 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Domn ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑏(-g‘𝑅)𝑐) ∈ 𝐵) |
22 | 21 | 3adant3r1 1184 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑏(-g‘𝑅)𝑐) ∈ 𝐵) |
23 | 22 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑏(-g‘𝑅)𝑐) ≠ 0 ) → (𝑏(-g‘𝑅)𝑐) ∈ 𝐵) |
24 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑏(-g‘𝑅)𝑐) ≠ 0 ) → (𝑏(-g‘𝑅)𝑐) ≠ 0 ) |
25 | | isdomn4.0 |
. . . . . . . . . 10
⊢ 0 =
(0g‘𝑅) |
26 | 2, 3, 25 | domnmuln0 20366 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ 𝐵 ∧ 𝑎 ≠ 0 ) ∧ ((𝑏(-g‘𝑅)𝑐) ∈ 𝐵 ∧ (𝑏(-g‘𝑅)𝑐) ≠ 0 )) → (𝑎 · (𝑏(-g‘𝑅)𝑐)) ≠ 0 ) |
27 | 14, 15, 18, 23, 24, 26 | syl122anc 1381 |
. . . . . . . 8
⊢ (((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) ∧ (𝑏(-g‘𝑅)𝑐) ≠ 0 ) → (𝑎 · (𝑏(-g‘𝑅)𝑐)) ≠ 0 ) |
28 | 27 | ex 416 |
. . . . . . 7
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑏(-g‘𝑅)𝑐) ≠ 0 → (𝑎 · (𝑏(-g‘𝑅)𝑐)) ≠ 0 )) |
29 | 28 | necon4d 2966 |
. . . . . 6
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎 · (𝑏(-g‘𝑅)𝑐)) = 0 → (𝑏(-g‘𝑅)𝑐) = 0 )) |
30 | 13, 29 | sylbird 263 |
. . . . 5
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (((𝑎 · 𝑏)(-g‘𝑅)(𝑎 · 𝑐)) = 0 → (𝑏(-g‘𝑅)𝑐) = 0 )) |
31 | 19 | adantr 484 |
. . . . . 6
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → 𝑅 ∈ Grp) |
32 | | id 22 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝐵) |
33 | 2, 3 | ringcl 19609 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 · 𝑏) ∈ 𝐵) |
34 | 5, 7, 32, 33 | syl3an 1162 |
. . . . . . 7
⊢ ((𝑅 ∈ Domn ∧ 𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵) → (𝑎 · 𝑏) ∈ 𝐵) |
35 | 34 | 3adant3r3 1186 |
. . . . . 6
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎 · 𝑏) ∈ 𝐵) |
36 | | id 22 |
. . . . . . . 8
⊢ (𝑐 ∈ 𝐵 → 𝑐 ∈ 𝐵) |
37 | 2, 3 | ringcl 19609 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑎 · 𝑐) ∈ 𝐵) |
38 | 5, 7, 36, 37 | syl3an 1162 |
. . . . . . 7
⊢ ((𝑅 ∈ Domn ∧ 𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑐 ∈ 𝐵) → (𝑎 · 𝑐) ∈ 𝐵) |
39 | 38 | 3adant3r2 1185 |
. . . . . 6
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (𝑎 · 𝑐) ∈ 𝐵) |
40 | 2, 25, 4 | grpsubeq0 18479 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ (𝑎 · 𝑏) ∈ 𝐵 ∧ (𝑎 · 𝑐) ∈ 𝐵) → (((𝑎 · 𝑏)(-g‘𝑅)(𝑎 · 𝑐)) = 0 ↔ (𝑎 · 𝑏) = (𝑎 · 𝑐))) |
41 | 31, 35, 39, 40 | syl3anc 1373 |
. . . . 5
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → (((𝑎 · 𝑏)(-g‘𝑅)(𝑎 · 𝑐)) = 0 ↔ (𝑎 · 𝑏) = (𝑎 · 𝑐))) |
42 | 2, 25, 4 | grpsubeq0 18479 |
. . . . . 6
⊢ ((𝑅 ∈ Grp ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → ((𝑏(-g‘𝑅)𝑐) = 0 ↔ 𝑏 = 𝑐)) |
43 | 31, 10, 11, 42 | syl3anc 1373 |
. . . . 5
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑏(-g‘𝑅)𝑐) = 0 ↔ 𝑏 = 𝑐)) |
44 | 30, 41, 43 | 3imtr3d 296 |
. . . 4
⊢ ((𝑅 ∈ Domn ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵)) → ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐)) |
45 | 44 | ralrimivvva 3115 |
. . 3
⊢ (𝑅 ∈ Domn →
∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐)) |
46 | 1, 45 | jca 515 |
. 2
⊢ (𝑅 ∈ Domn → (𝑅 ∈ NzRing ∧
∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐))) |
47 | | nzrring 20329 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Ring) |
48 | 47 | ringgrpd 19601 |
. . . . . . . . . 10
⊢ (𝑅 ∈ NzRing → 𝑅 ∈ Grp) |
49 | 2, 25 | grpidcl 18425 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Grp → 0 ∈ 𝐵) |
50 | 48, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ NzRing → 0 ∈ 𝐵) |
51 | 50 | adantr 484 |
. . . . . . . 8
⊢ ((𝑅 ∈ NzRing ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵)) → 0 ∈ 𝐵) |
52 | | oveq2 7242 |
. . . . . . . . . . 11
⊢ (𝑐 = 0 → (𝑎 · 𝑐) = (𝑎 · 0 )) |
53 | 52 | eqeq2d 2750 |
. . . . . . . . . 10
⊢ (𝑐 = 0 → ((𝑎 · 𝑏) = (𝑎 · 𝑐) ↔ (𝑎 · 𝑏) = (𝑎 · 0 ))) |
54 | | eqeq2 2751 |
. . . . . . . . . 10
⊢ (𝑐 = 0 → (𝑏 = 𝑐 ↔ 𝑏 = 0 )) |
55 | 53, 54 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑐 = 0 → (((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐) ↔ ((𝑎 · 𝑏) = (𝑎 · 0 ) → 𝑏 = 0 ))) |
56 | 55 | rspcv 3546 |
. . . . . . . 8
⊢ ( 0 ∈ 𝐵 → (∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐) → ((𝑎 · 𝑏) = (𝑎 · 0 ) → 𝑏 = 0 ))) |
57 | 51, 56 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ NzRing ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵)) → (∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐) → ((𝑎 · 𝑏) = (𝑎 · 0 ) → 𝑏 = 0 ))) |
58 | 2, 3, 25 | ringrz 19636 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵) → (𝑎 · 0 ) = 0 ) |
59 | 47, 7, 58 | syl2an 599 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ NzRing ∧ 𝑎 ∈ (𝐵 ∖ { 0 })) → (𝑎 · 0 ) = 0 ) |
60 | 59 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝑅 ∈ NzRing ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵)) → (𝑎 · 0 ) = 0 ) |
61 | 60 | eqeq2d 2750 |
. . . . . . . 8
⊢ ((𝑅 ∈ NzRing ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵)) → ((𝑎 · 𝑏) = (𝑎 · 0 ) ↔ (𝑎 · 𝑏) = 0 )) |
62 | 61 | imbi1d 345 |
. . . . . . 7
⊢ ((𝑅 ∈ NzRing ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵)) → (((𝑎 · 𝑏) = (𝑎 · 0 ) → 𝑏 = 0 ) ↔ ((𝑎 · 𝑏) = 0 → 𝑏 = 0 ))) |
63 | 57, 62 | sylibd 242 |
. . . . . 6
⊢ ((𝑅 ∈ NzRing ∧ (𝑎 ∈ (𝐵 ∖ { 0 }) ∧ 𝑏 ∈ 𝐵)) → (∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐) → ((𝑎 · 𝑏) = 0 → 𝑏 = 0 ))) |
64 | 63 | ralimdvva 3104 |
. . . . 5
⊢ (𝑅 ∈ NzRing →
(∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐) → ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → 𝑏 = 0 ))) |
65 | | isdomn5 39930 |
. . . . 5
⊢
(∀𝑎 ∈
𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 )) ↔ ∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → 𝑏 = 0 )) |
66 | 64, 65 | syl6ibr 255 |
. . . 4
⊢ (𝑅 ∈ NzRing →
(∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 )))) |
67 | 66 | imdistani 572 |
. . 3
⊢ ((𝑅 ∈ NzRing ∧
∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐)) → (𝑅 ∈ NzRing ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 )))) |
68 | 2, 3, 25 | isdomn 20362 |
. . 3
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 · 𝑏) = 0 → (𝑎 = 0 ∨ 𝑏 = 0 )))) |
69 | 67, 68 | sylibr 237 |
. 2
⊢ ((𝑅 ∈ NzRing ∧
∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐)) → 𝑅 ∈ Domn) |
70 | 46, 69 | impbii 212 |
1
⊢ (𝑅 ∈ Domn ↔ (𝑅 ∈ NzRing ∧
∀𝑎 ∈ (𝐵 ∖ { 0 })∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ((𝑎 · 𝑏) = (𝑎 · 𝑐) → 𝑏 = 𝑐))) |