Proof of Theorem drngmul0or
Step | Hyp | Ref
| Expression |
1 | | df-ne 2944 |
. . . . 5
⊢ (𝑋 ≠ 0 ↔ ¬ 𝑋 = 0 ) |
2 | | oveq2 7283 |
. . . . . . . 8
⊢ ((𝑋 · 𝑌) = 0 →
(((invr‘𝑅)‘𝑋) · (𝑋 · 𝑌)) = (((invr‘𝑅)‘𝑋) · 0 )) |
3 | 2 | ad2antlr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 · 𝑌) = 0 ) ∧ 𝑋 ≠ 0 ) →
(((invr‘𝑅)‘𝑋) · (𝑋 · 𝑌)) = (((invr‘𝑅)‘𝑋) · 0 )) |
4 | | drngmuleq0.r |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ DivRing) |
5 | 4 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → 𝑅 ∈ DivRing) |
6 | | drngmuleq0.x |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
7 | 6 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝐵) |
8 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 ) |
9 | | drngmuleq0.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑅) |
10 | | drngmuleq0.o |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝑅) |
11 | | drngmuleq0.t |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑅) |
12 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) |
13 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(invr‘𝑅) = (invr‘𝑅) |
14 | 9, 10, 11, 12, 13 | drnginvrl 20010 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) →
(((invr‘𝑅)‘𝑋) · 𝑋) = (1r‘𝑅)) |
15 | 5, 7, 8, 14 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) →
(((invr‘𝑅)‘𝑋) · 𝑋) = (1r‘𝑅)) |
16 | 15 | oveq1d 7290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) →
((((invr‘𝑅)‘𝑋) · 𝑋) · 𝑌) = ((1r‘𝑅) · 𝑌)) |
17 | | drngring 19998 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ DivRing → 𝑅 ∈ Ring) |
18 | 4, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ∈ Ring) |
19 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → 𝑅 ∈ Ring) |
20 | 9, 10, 13 | drnginvrcl 20008 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ DivRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) →
((invr‘𝑅)‘𝑋) ∈ 𝐵) |
21 | 5, 7, 8, 20 | syl3anc 1370 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) →
((invr‘𝑅)‘𝑋) ∈ 𝐵) |
22 | | drngmuleq0.y |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
23 | 22 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → 𝑌 ∈ 𝐵) |
24 | 9, 11 | ringass 19803 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧
(((invr‘𝑅)‘𝑋) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((((invr‘𝑅)‘𝑋) · 𝑋) · 𝑌) = (((invr‘𝑅)‘𝑋) · (𝑋 · 𝑌))) |
25 | 19, 21, 7, 23, 24 | syl13anc 1371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) →
((((invr‘𝑅)‘𝑋) · 𝑋) · 𝑌) = (((invr‘𝑅)‘𝑋) · (𝑋 · 𝑌))) |
26 | 9, 11, 12 | ringlidm 19810 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵) → ((1r‘𝑅) · 𝑌) = 𝑌) |
27 | 18, 22, 26 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 →
((1r‘𝑅)
·
𝑌) = 𝑌) |
28 | 27 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) →
((1r‘𝑅)
·
𝑌) = 𝑌) |
29 | 16, 25, 28 | 3eqtr3d 2786 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) →
(((invr‘𝑅)‘𝑋) · (𝑋 · 𝑌)) = 𝑌) |
30 | 29 | adantlr 712 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 · 𝑌) = 0 ) ∧ 𝑋 ≠ 0 ) →
(((invr‘𝑅)‘𝑋) · (𝑋 · 𝑌)) = 𝑌) |
31 | 18 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑋 · 𝑌) = 0 ) → 𝑅 ∈ Ring) |
32 | 31 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 · 𝑌) = 0 ) ∧ 𝑋 ≠ 0 ) → 𝑅 ∈ Ring) |
33 | 21 | adantlr 712 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑋 · 𝑌) = 0 ) ∧ 𝑋 ≠ 0 ) →
((invr‘𝑅)‘𝑋) ∈ 𝐵) |
34 | 9, 11, 10 | ringrz 19827 |
. . . . . . . 8
⊢ ((𝑅 ∈ Ring ∧
((invr‘𝑅)‘𝑋) ∈ 𝐵) → (((invr‘𝑅)‘𝑋) · 0 ) = 0 ) |
35 | 32, 33, 34 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑋 · 𝑌) = 0 ) ∧ 𝑋 ≠ 0 ) →
(((invr‘𝑅)‘𝑋) · 0 ) = 0 ) |
36 | 3, 30, 35 | 3eqtr3d 2786 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑋 · 𝑌) = 0 ) ∧ 𝑋 ≠ 0 ) → 𝑌 = 0 ) |
37 | 36 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ (𝑋 · 𝑌) = 0 ) → (𝑋 ≠ 0 → 𝑌 = 0 )) |
38 | 1, 37 | syl5bir 242 |
. . . 4
⊢ ((𝜑 ∧ (𝑋 · 𝑌) = 0 ) → (¬ 𝑋 = 0 → 𝑌 = 0 )) |
39 | 38 | orrd 860 |
. . 3
⊢ ((𝜑 ∧ (𝑋 · 𝑌) = 0 ) → (𝑋 = 0 ∨ 𝑌 = 0 )) |
40 | 39 | ex 413 |
. 2
⊢ (𝜑 → ((𝑋 · 𝑌) = 0 → (𝑋 = 0 ∨ 𝑌 = 0 ))) |
41 | 9, 11, 10 | ringlz 19826 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵) → ( 0 · 𝑌) = 0 ) |
42 | 18, 22, 41 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ( 0 · 𝑌) = 0 ) |
43 | | oveq1 7282 |
. . . . 5
⊢ (𝑋 = 0 → (𝑋 · 𝑌) = ( 0 · 𝑌)) |
44 | 43 | eqeq1d 2740 |
. . . 4
⊢ (𝑋 = 0 → ((𝑋 · 𝑌) = 0 ↔ ( 0 · 𝑌) = 0 )) |
45 | 42, 44 | syl5ibrcom 246 |
. . 3
⊢ (𝜑 → (𝑋 = 0 → (𝑋 · 𝑌) = 0 )) |
46 | 9, 11, 10 | ringrz 19827 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 ) |
47 | 18, 6, 46 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝑋 · 0 ) = 0 ) |
48 | | oveq2 7283 |
. . . . 5
⊢ (𝑌 = 0 → (𝑋 · 𝑌) = (𝑋 · 0 )) |
49 | 48 | eqeq1d 2740 |
. . . 4
⊢ (𝑌 = 0 → ((𝑋 · 𝑌) = 0 ↔ (𝑋 · 0 ) = 0 )) |
50 | 47, 49 | syl5ibrcom 246 |
. . 3
⊢ (𝜑 → (𝑌 = 0 → (𝑋 · 𝑌) = 0 )) |
51 | 45, 50 | jaod 856 |
. 2
⊢ (𝜑 → ((𝑋 = 0 ∨ 𝑌 = 0 ) → (𝑋 · 𝑌) = 0 )) |
52 | 40, 51 | impbid 211 |
1
⊢ (𝜑 → ((𝑋 · 𝑌) = 0 ↔ (𝑋 = 0 ∨ 𝑌 = 0 ))) |